Theorem mpbiran2 941

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)

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

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  reueq  2938  ss0b  3464  eusv1  4454  eusv2nf  4458  eusv2  4459  opthprc  4679  opelres  4914  f1cnvcnv  5434  fores  5449  f1orn  5473  funfvdm  5581  dfoprab2  5924  tpostpos  6267  opelreal  7828  elreal2  7831  eqresr  7837  axprecex  7881  zeoxor  11876  isprm2  12119  toptopon  13557  bdeq0  14658  subctctexmid  14789