Theorem mpbiran2 910

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  914  reueq  3159  ss0b  3670  eusv1  4489  eusv2nf  4493  eusv2  4494  opthprc  4889  sosn  4911  opelres  5119  fdmrn  5576  f1cnvcnv  5617  fores  5632  f1orn  5654  funfv  5761  dfoprab2  6136  elxp7  6612  tpostpos  6768  dfsup2OLD  7696  canthwe  8821  recmulnq  9136  opelreal  9300  elreal2  9302  eqresr  9307  elnn1uz2  10934  faclbnd4lem1  12072  isprm2  13774  joindm  15176  meetdm  15190  symgbas0  15902  efgs1  16235  funsnfsupOLD  17673  toptopon  18541  ist1-3  18956  perfcls  18972  prdsxmetlem  19946  hhsssh2  24674  choc0  24732  chocnul  24734  shlesb1i  24792  adjeu  25296  isarchi  26202  derang0  27060  nofulllem5  27850  brtxp  27914  brpprod  27919  dfon3  27926  brtxpsd  27928  topmeet  28588  filnetlem2  28603  filnetlem3  28604  fdc  28644  0totbnd  28675  heiborlem3  28715  bj-rabtrALT  32436  bj-snsetex  32459