Theorem pm3.26bi 322

Description: Deduction eliminating a conjunct.

Hypothesis

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

Assertion

Ref	Expression
pm3.26bi	|- (ph -> ps)

Proof of Theorem pm3.26bi

Step	Hyp	Ref	Expression
1		pm3.26bi.1	. . 3 |- (ph <-> (ps /\ ch))
2	1	biimp 151	. 2 |- (ph -> (ps /\ ch))
3	2	pm3.26d 321	1 |- (ph -> ps)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  3simpa 784  pssss 2139  eldifi 2158  inss1 2226  pwssun 2822  sopo 2846  wefr 2934  ordtr 2957  omsson 3131  relop 3270  dmcoss 3355  opres 3367  funrel 3525  fnfun 3577  ffn 3619  f1f 3656  f1of1 3679  f1ofo 3686  nfvres 3739  dff2 3808  isof1o 3884  eqop 4094  xpopth 4096  1st2nd 4098  sdomdom 4373  mapxpen 4481  xpmapenlem3 4484  xpmapenlem4 4485  xpmapenlem5 4486  inf3lemd 4592  rankpw 4664  aceq3lem 4712  aceq5lem4 4718  cardinfima 4871  suppsr3 5204  eqle 5563  zret 6094  nnssz 6106  dfuz 6158  uzwo3lem2 6173  sqrlem12 6622  sqrlem13 6623  iserzshft2 7052  mulc1cncf 7222  ivthlem6 7229  ivthlem7 7230  ivthlem4OLD 7236  ivthlem6OLD 7238  ivthlem7OLD 7239  haustop 7736  cmsmet 7912  xplmi 7923  xplmi2 7924  oprcn 7927  bopcnlem2 7932  bopcnlem3 7933  fsumcnlem 7939  ablgrp 8053  nmogtmnf 8378  bnnv 8470  hlbn 8536  pilem2 8610  pilem3 8611  circgrpOLD 8677  eff1i 8683  effoi 8684  hcauseq 8991  hlimseq 8996  hlimvec 8997  shss 9018  sh0 9023  projlem21 9145  projlem26 9150  projlem29 9153  projlem30 9154  lnopft 9725  bdoplnt 9728  nmopgtmnf 9735  hmopft 9741  lnfnft 9751  unopf1ot 9779  elunop2t 9876  rnbra 9978  elpjhmopt 10051  stclt 10081  stge0t 10089  stle1t 10090  stcltrlem1 10141  mdslle1 10181  mdslle2 10182  filintf 10479

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain