Theorem mpbiran2 954

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

Syntax hints:   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  pm5.62  958  reueq  3404  ss0b  3973  eusv1  4860  eusv2nf  4864  eusv2  4865  opthprc  5167  sosn  5188  opelres  5401  fdmrn  6064  f1cnvcnv  6109  fores  6124  f1orn  6147  funfv  6265  dfoprab2  6701  elxp7  7201  tpostpos  7372  canthwe  9473  recmulnq  9786  opelreal  9951  elreal2  9953  eqresr  9958  elnn1uz2  11765  faclbnd4lem1  13080  isprm2  15395  joindm  17003  meetdm  17017  symgbas0  17814  efgs1  18148  toptopon  20722  ist1-3  21153  perfcls  21169  prdsxmetlem  22173  rusgrprc  26486  hhsssh2  28127  choc0  28185  chocnul  28187  shlesb1i  28245  adjeu  28748  isarchi  29736  derang0  31151  brtxp  31987  brpprod  31992  dfon3  31999  brtxpsd  32001  topmeet  32359  filnetlem2  32374  filnetlem3  32375  bj-rabtrALT  32927  bj-snsetex  32951  relowlpssretop  33212  poimirlem28  33437  fdc  33541  0totbnd  33572  heiborlem3  33612  ifpid3g  37837  elintima  37945