Theorem mpbiran2 943

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  2959  ss0b  3486  eusv1  4483  eusv2nf  4487  eusv2  4488  opthprc  4710  opelres  4947  f1cnvcnv  5470  fores  5486  f1orn  5510  funfvdm  5620  dfoprab2  5965  tpostpos  6317  opelreal  7887  elreal2  7890  eqresr  7896  axprecex  7940  zeoxor  12010  isprm2  12255  toptopon  14186  bdeq0  15359  subctctexmid  15491