Theorem mpbiran 882

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.)

Hypotheses

Ref	Expression
mpbiran.1	|- ps
mpbiran.2	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
mpbiran	|- ( ph <-> ch )

Proof of Theorem mpbiran

Step	Hyp	Ref	Expression
1		mpbiran.2	. 2 |- ( ph <-> ( ps /\ ch ) )
2		mpbiran.1	. . 3 |- ps
3	2	biantrur 297	. 2 |- ( ch <-> ( ps /\ ch ) )
4	1, 3	bitr4i 185	1 |- ( ph <-> ch )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpbir2an  884  unssdif  3215  unssin  3219  inssun  3220  invdif  3222  exmidexmid  3987  opabm  4063  regexmidlem1  4304  elirr  4312  en2lp  4325  wessep  4348  peano5  4367  relop  4534  ssrnres  4813  funopab  4985  funcnv2  5010  funcnveq  5013  fnres  5066  idref  5448  rnoprab  5638  djulf1o  6554  djurf1o  6555  lbfzo0  9319