Theorem mpbiran2 950

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  3006  ss0b  3536  eusv1  4555  eusv2nf  4559  eusv2  4560  opthprc  4783  opelres  5024  f1cnvcnv  5562  fores  5578  f1orn  5602  funfvdm  5718  dfoprab2  6078  tpostpos  6473  opelreal  8090  elreal2  8093  eqresr  8099  axprecex  8143  zeoxor  12493  isprm2  12752  toptopon  14812  bdeq0  16566  subctctexmid  16705