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  2972  ss0b  3500  eusv1  4499  eusv2nf  4503  eusv2  4504  opthprc  4726  opelres  4964  f1cnvcnv  5492  fores  5508  f1orn  5532  funfvdm  5642  dfoprab2  5992  tpostpos  6350  opelreal  7940  elreal2  7943  eqresr  7949  axprecex  7993  zeoxor  12180  isprm2  12439  toptopon  14490  bdeq0  15803  subctctexmid  15937