Theorem mpbiran2 917

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)

Hypotheses

Ref	Expression
mpbiran2.1	|- ch
mpbiran2.2	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
mpbiran2	|- ( ph <-> ps )

Proof of Theorem mpbiran2

Step	Hyp	Ref	Expression
1		mpbiran2.2	. 2 |- ( ph <-> ( ps /\ ch ) )
2		mpbiran2.1	. . 3 |- ch
3	2	biantru 505	. 2 |- ( ps <-> ( ps /\ ch ) )
4	1, 3	bitr4i 252	1 |- ( ph <-> ps )

Syntax hints:   <-> wb 184   /\ wa 369

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

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  pm5.62  921  reueq  3301  ss0b  3815  eusv1  4641  eusv2nf  4645  eusv2  4646  opthprc  5046  sosn  5068  opelres  5277  fdmrn  5744  f1cnvcnv  5787  fores  5802  f1orn  5824  funfv  5932  dfoprab2  6325  elxp7  6814  tpostpos  6972  dfsup2OLD  7899  canthwe  9025  recmulnq  9338  opelreal  9503  elreal2  9505  eqresr  9510  elnn1uz2  11154  faclbnd4lem1  12335  isprm2  14080  joindm  15486  meetdm  15500  symgbas0  16214  efgs1  16549  funsnfsupOLD  18027  toptopon  19201  ist1-3  19616  perfcls  19632  prdsxmetlem  20606  hhsssh2  25862  choc0  25920  chocnul  25922  shlesb1i  25980  adjeu  26484  isarchi  27388  derang0  28253  nofulllem5  29043  brtxp  29107  brpprod  29112  dfon3  29119  brtxpsd  29121  topmeet  29785  filnetlem2  29800  filnetlem3  29801  fdc  29841  0totbnd  29872  heiborlem3  29912  bj-rabtrALT  33579  bj-snsetex  33602