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  3016  ss0b  3548  eusv1  4573  eusv2nf  4577  eusv2  4578  opthprc  4801  opelres  5043  f1cnvcnv  5584  fores  5600  f1orn  5624  funfvdm  5740  dfoprab2  6100  tpostpos  6495  opelreal  8142  elreal2  8145  eqresr  8151  axprecex  8195  zeoxor  12555  isprm2  12814  toptopon  14883  bdeq0  16637  subctctexmid  16774