Theorem mpbiran 884

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)

Hypotheses

Ref	Expression
mpbiran.1	|- ps
mpbiran.2	|- (ph <-> (ps /\ ch))

Assertion

Ref	Expression
mpbiran	|- (ph <-> ch)

Proof of Theorem mpbiran

Step	Hyp	Ref	Expression
1		mpbiran.2	. 2 |- (ph <-> (ps /\ ch))
2		mpbiran.1	. . 3 |- ps
3	2	biantrur 492	. 2 |- (ch <-> (ps /\ ch))
4	1, 3	bitr4i 243	1 |- (ph <-> ch)

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:  mpbir2an  886  pm5.63  890  ddif  3399  dfun2  3491  dfin2  3492  0pss  3589  pssv  3591  disj4  3600  cnvkexg  4287  ssetkex  4295  sikexg  4297  ins2kexg  4306  ins3kexg  4307  nnsucelrlem1  4425  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  opabn0  4717  setconslem6  4737  fnres  5200  dmsi  5520  otelins2  5792  composeex  5821  dmpprod  5841  crossex  5851  transex  5911  enmap2  6069  csucex  6260  nmembers1lem1  6269  nchoicelem18  6307  dmfrec  6317  fnfreclem1  6318