Theorem pm3.27bd 263

Description: Deduction eliminating a conjunct.

Hypothesis

Ref	Expression
pm3.27bd.1	|- (ph <-> (ps /\ ch))

Assertion

Ref	Expression
pm3.27bd	|- (ph -> ch)

Proof of Theorem pm3.27bd

Step	Hyp	Ref	Expression
1		pm3.27bd.1	. . 3 |- (ph <-> (ps /\ ch))
2	1	biimp 133	. 2 |- (ph -> (ps /\ ch))
3	2	pm3.27d 262	1 |- (ph -> ch)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  sb1 858  eumo 1037  2eu1 1067  eldifn 1592  opth2 1909  pwssun 1917  unisseq 1946  ssintub 1981  weso 2192  ordwe 2212  tfis 2245  onminsb 2264  onminesb 2265  limomss 2378  ordom 2382  ssnlim 2407  funmo 2680  funss 2682  funeu 2685  funsn 2690  funco 2696  funun 2700  fununi 2705  funimaexg 2715  fndm 2723  fnopabg 2745  frn 2757  forn 2789  f1o2 2804  f1f1orn 2810  f1imacnv 2814  f1ococnv2 2817  f1fveq 2918  isorel 2932  f1oweOLD 2944  tz7.48lem 2993  eceqopreq 3249  sdomnen 3291  en0 3328  en1 3331  canth2 3381  mapenlem1 3384  mapunen 3397  phplem5 3407  php3 3411  ssfi 3430  fiint 3445  inf3lem2 3465  inf3lem6 3469  inf3lem7 3470  inf5 3472  tz9.12lem3 3505  rankr1 3518  scottex 3541  aceq5lem4 3561  aceq5lem5 3562  ac6 3576  kmlem1 3580  zornlem2 3604  zorn2 3612  fodomb 3615  oncardid 3628  cardid 3635  ondomcard 3663  iscard3 3693  0npi 3804  mulcanpi 3821  nlt1pi 3827  prcdpq 3891  prnmax 3893  suppsr3 4018  add20 4329  uzwo 4605  seqrn 4673  sqrlem12 4742  facclt 4874  climconv 4880  ruclem23 4907  ruc 4924  nn0ennn 4925  cauchyconv 5105  hlimconv 5111  shaddclt 5123  shmulclt 5124  chlim 5139  chcompl 5150  occl 5188  projlem15 5207  projlem22 5214  projlem26 5218  choc1 5292  sthil 5675  stjt 5676  atcv0 5740  chpssat 5756

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org