Theorem mpbiran2 954

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  3025  ss0b  3562  eusv1  4593  eusv2nf  4597  eusv2  4598  opthprc  4821  opelres  5063  f1cnvcnv  5604  fores  5620  f1orn  5644  funfvdm  5760  fdmrn  6024  dfoprab2  6125  tpostpos  6525  opelreal  8184  elreal2  8187  eqresr  8193  axprecex  8237  zeoxor  12614  isprm2  12873  toptopon  15042  bdeq0  16807  subctctexmid  16944