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 503	. 2 |- ( ps <-> ( ps /\ ch ) )
4	1, 3	bitr4i 252	1 |- ( ph <-> ps )

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

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 369

This theorem is referenced by:  pm5.62  921  reueq  3235  ss0b  3755  eusv1  4572  eusv2nf  4576  eusv2  4577  opthprc  4974  sosn  4996  opelres  5204  fdmrn  5667  f1cnvcnv  5710  fores  5725  f1orn  5747  funfv  5854  dfoprab2  6260  elxp7  6750  tpostpos  6911  dfsup2OLD  7836  canthwe  8958  recmulnq  9271  opelreal  9436  elreal2  9438  eqresr  9443  elnn1uz2  11095  faclbnd4lem1  12292  isprm2  14246  joindm  15769  meetdm  15783  symgbas0  16555  efgs1  16889  funsnfsupOLD  18388  toptopon  19538  ist1-3  19955  perfcls  19971  prdsxmetlem  20975  hhsssh2  26324  choc0  26382  chocnul  26384  shlesb1i  26442  adjeu  26945  isarchi  27909  derang0  28838  nofulllem5  29667  brtxp  29719  brpprod  29724  dfon3  29731  brtxpsd  29733  topmeet  30384  filnetlem2  30399  filnetlem3  30400  fdc  30440  0totbnd  30471  heiborlem3  30511  bj-rabtrALT  34881  bj-snsetex  34904  ifpid3g  38159  elintima  38230