Theorem mpbiran2 926

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 300	. 2 |- ( ps <-> ( ps /\ ch ) )
4	1, 3	bitr4i 186	1 |- ( ph <-> ps )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  reueq  2907  ss0b  3429  eusv1  4406  eusv2nf  4410  eusv2  4411  opthprc  4630  opelres  4864  f1cnvcnv  5379  fores  5394  f1orn  5417  funfvdm  5524  dfoprab2  5858  tpostpos  6201  opelreal  7726  elreal2  7729  eqresr  7735  axprecex  7779  zeoxor  11733  isprm2  11966  toptopon  12363  bdeq0  13388  subctctexmid  13520