Theorem mpbiran2 885

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

Syntax hints:   <-> wb 176   /\ wa 358

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 177  df-an 360

This theorem is referenced by:  pm5.62  889  reueq  3033  ss0b  3580  dfimak2  4298  dfpw2  4327  ltfinex  4464  ssfin  4470  eqpw1relk  4479  ncfinraiselem2  4480  eqtfinrelk  4486  evenodddisjlem1  4515  nnadjoinlem1  4519  tfinnnlem1  4533  dfphi2  4569  dfop2lem1  4573  setconslem2  4732  setconslem4  4734  f1funfun  5263  fores  5278  funfv  5375  otelins3  5792  releqmpt  5808  releqmpt2  5809  fnsex  5832  foundex  5914  enmap2lem1  6063  enmap1lem1  6069  fnce  6176  sbthlem1  6203  sbthlem3  6205  tcfnex  6244  nncdiv3lem2  6276  nchoicelem9  6297  nchoicelem11  6299