Theorem mpbiran2 903

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 502	. 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  907  reueq  3145  ss0b  3655  eusv1  4474  eusv2nf  4478  eusv2  4479  opthprc  4873  sosn  4895  opelres  5103  fdmrn  5561  f1cnvcnv  5602  fores  5617  f1orn  5639  funfv  5746  dfoprab2  6122  elxp7  6598  tpostpos  6754  dfsup2OLD  7681  canthwe  8806  recmulnq  9121  opelreal  9285  elreal2  9287  eqresr  9292  elnn1uz2  10919  faclbnd4lem1  12053  isprm2  13754  joindm  15156  meetdm  15170  symgbas0  15879  efgs1  16212  funsnfsupOLD  17569  toptopon  18380  ist1-3  18795  perfcls  18811  prdsxmetlem  19785  hhsssh2  24494  choc0  24552  chocnul  24554  shlesb1i  24612  adjeu  25116  isarchi  26023  derang0  26905  nofulllem5  27694  brtxp  27758  brpprod  27763  dfon3  27770  brtxpsd  27772  topmeet  28429  filnetlem2  28444  filnetlem3  28445  fdc  28485  0totbnd  28516  heiborlem3  28556  bj-rabtrALT  32040  bj-snsetex  32060