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  2963  ss0b  3491  eusv1  4488  eusv2nf  4492  eusv2  4493  opthprc  4715  opelres  4952  f1cnvcnv  5477  fores  5493  f1orn  5517  funfvdm  5627  dfoprab2  5973  tpostpos  6331  opelreal  7911  elreal2  7914  eqresr  7920  axprecex  7964  zeoxor  12051  isprm2  12310  toptopon  14338  bdeq0  15597  subctctexmid  15731