Theorem mpbiran2 936

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  2929  ss0b  3454  eusv1  4437  eusv2nf  4441  eusv2  4442  opthprc  4662  opelres  4896  f1cnvcnv  5414  fores  5429  f1orn  5452  funfvdm  5559  dfoprab2  5900  tpostpos  6243  opelreal  7789  elreal2  7792  eqresr  7798  axprecex  7842  zeoxor  11828  isprm2  12071  toptopon  12810  bdeq0  13902  subctctexmid  14034