Theorem mpbiran2 935

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

Syntax hints:   <-> wb 189   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  pm5.62  939  reueq  3248  ss0b  3776  eusv1  4614  eusv2nf  4618  eusv2  4619  opthprc  4904  sosn  4926  opelres  5132  fdmrn  5771  f1cnvcnv  5814  fores  5829  f1orn  5851  funfv  5960  dfoprab2  6369  elxp7  6858  tpostpos  7024  canthwe  9107  recmulnq  9420  opelreal  9585  elreal2  9587  eqresr  9592  elnn1uz2  11269  faclbnd4lem1  12516  isprm2  14687  joindm  16304  meetdm  16318  symgbas0  17090  efgs1  17440  toptopon  20003  ist1-3  20420  perfcls  20436  prdsxmetlem  21438  hhsssh2  26977  choc0  27035  chocnul  27037  shlesb1i  27095  adjeu  27598  isarchi  28550  derang0  29942  nofulllem5  30645  brtxp  30697  brpprod  30702  dfon3  30709  brtxpsd  30711  topmeet  31070  filnetlem2  31085  filnetlem3  31086  bj-rabtrALT  31580  bj-snsetex  31603  relowlpssretop  31813  poimirlem28  32014  fdc  32120  0totbnd  32151  heiborlem3  32191  ifpid3g  36182  elintima  36291  rusgrprc  39751