Theorem mpbiran2 926

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  reueq  2887  ss0b  3407  eusv1  4381  eusv2nf  4385  eusv2  4386  opthprc  4598  opelres  4832  f1cnvcnv  5347  fores  5362  f1orn  5385  funfvdm  5492  dfoprab2  5826  tpostpos  6169  opelreal  7659  elreal2  7662  eqresr  7668  axprecex  7712  zeoxor  11602  isprm2  11834  toptopon  12224  bdeq0  13236  subctctexmid  13369