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  3281  ss0b  3798  eusv1  4628  eusv2nf  4632  eusv2  4633  opthprc  5034  sosn  5056  opelres  5266  fdmrn  5733  f1cnvcnv  5776  fores  5791  f1orn  5813  funfv  5922  dfoprab2  6325  elxp7  6815  tpostpos  6974  dfsup2OLD  7902  canthwe  9029  recmulnq  9342  opelreal  9507  elreal2  9509  eqresr  9514  elnn1uz2  11164  faclbnd4lem1  12347  isprm2  14099  joindm  15504  meetdm  15518  symgbas0  16290  efgs1  16624  funsnfsupOLD  18127  toptopon  19304  ist1-3  19720  perfcls  19736  prdsxmetlem  20741  hhsssh2  26055  choc0  26113  chocnul  26115  shlesb1i  26173  adjeu  26677  isarchi  27596  derang0  28483  nofulllem5  29438  brtxp  29502  brpprod  29507  dfon3  29514  brtxpsd  29516  topmeet  30154  filnetlem2  30169  filnetlem3  30170  fdc  30210  0totbnd  30241  heiborlem3  30281  bj-rabtrALT  34231  bj-snsetex  34254