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  2971  ss0b  3499  eusv1  4498  eusv2nf  4502  eusv2  4503  opthprc  4725  opelres  4963  f1cnvcnv  5491  fores  5507  f1orn  5531  funfvdm  5641  dfoprab2  5991  tpostpos  6349  opelreal  7939  elreal2  7942  eqresr  7948  axprecex  7992  zeoxor  12151  isprm2  12410  toptopon  14461  bdeq0  15765  subctctexmid  15899