Theorem mpbiran2 947

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  3003  ss0b  3532  eusv1  4547  eusv2nf  4551  eusv2  4552  opthprc  4775  opelres  5016  f1cnvcnv  5550  fores  5566  f1orn  5590  funfvdm  5705  dfoprab2  6063  tpostpos  6425  opelreal  8037  elreal2  8040  eqresr  8046  axprecex  8090  zeoxor  12420  isprm2  12679  toptopon  14732  bdeq0  16398  subctctexmid  16537