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  3002  ss0b  3531  eusv1  4542  eusv2nf  4546  eusv2  4547  opthprc  4769  opelres  5009  f1cnvcnv  5541  fores  5557  f1orn  5581  funfvdm  5696  dfoprab2  6050  tpostpos  6408  opelreal  8010  elreal2  8013  eqresr  8019  axprecex  8063  zeoxor  12375  isprm2  12634  toptopon  14686  bdeq0  16188  subctctexmid  16325