Theorem mpbiran2 931

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  2925  ss0b  3448  eusv1  4430  eusv2nf  4434  eusv2  4435  opthprc  4655  opelres  4889  f1cnvcnv  5404  fores  5419  f1orn  5442  funfvdm  5549  dfoprab2  5889  tpostpos  6232  opelreal  7768  elreal2  7771  eqresr  7777  axprecex  7821  zeoxor  11806  isprm2  12049  toptopon  12656  bdeq0  13749  subctctexmid  13881