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  3034  ss0b  3581  dfimak2  4299  dfpw2  4328  ltfinex  4465  ssfin  4471  eqpw1relk  4480  ncfinraiselem2  4481  eqtfinrelk  4487  evenodddisjlem1  4516  nnadjoinlem1  4520  tfinnnlem1  4534  dfphi2  4570  dfop2lem1  4574  setconslem2  4733  setconslem4  4735  f1funfun  5264  fores  5279  funfv  5376  otelins3  5793  releqmpt  5809  releqmpt2  5810  fnsex  5833  foundex  5915  enmap2lem1  6064  enmap1lem1  6070  fnce  6177  sbthlem1  6204  sbthlem3  6206  tcfnex  6245  nncdiv3lem2  6277  nchoicelem9  6298  nchoicelem11  6300