Theorem mpbiran2 927

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

Syntax hints:   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  pm5.62  931  reueq  3268  ss0b  3794  eusv1  4618  eusv2nf  4622  eusv2  4623  opthprc  4901  sosn  4923  opelres  5129  fdmrn  5761  f1cnvcnv  5804  fores  5819  f1orn  5841  funfv  5948  dfoprab2  6351  elxp7  6840  tpostpos  7004  canthwe  9083  recmulnq  9396  opelreal  9561  elreal2  9563  eqresr  9568  elnn1uz2  11242  faclbnd4lem1  12484  isprm2  14631  joindm  16248  meetdm  16262  symgbas0  17034  efgs1  17384  toptopon  19946  ist1-3  20363  perfcls  20379  prdsxmetlem  21381  hhsssh2  26919  choc0  26977  chocnul  26979  shlesb1i  27037  adjeu  27540  isarchi  28506  derang0  29900  nofulllem5  30600  brtxp  30652  brpprod  30657  dfon3  30664  brtxpsd  30666  topmeet  31025  filnetlem2  31040  filnetlem3  31041  bj-rabtrALT  31503  bj-snsetex  31525  relowlpssretop  31731  poimirlem28  31932  fdc  32038  0totbnd  32069  heiborlem3  32109  ifpid3g  36106  elintima  36215