Theorem mpbiran2 944

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  2979  ss0b  3508  eusv1  4517  eusv2nf  4521  eusv2  4522  opthprc  4744  opelres  4983  f1cnvcnv  5514  fores  5530  f1orn  5554  funfvdm  5665  dfoprab2  6015  tpostpos  6373  opelreal  7975  elreal2  7978  eqresr  7984  axprecex  8028  zeoxor  12295  isprm2  12554  toptopon  14605  bdeq0  16002  subctctexmid  16139