Theorem mpbiran 949

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

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:  mpbir2an  951  unssdif  3444  unssin  3448  inssun  3449  invdif  3451  pwpwab  4063  exmidexmid  4292  opabm  4381  regexmidlem1  4637  elirr  4645  en2lp  4658  wessep  4682  peano5  4702  relop  4886  ssrnres  5186  funopab  5368  funcnv2  5397  funcnveq  5400  fnres  5456  idref  5907  rnoprab  6114  elixp  6917  djuf1olem  7295  lbfzo0  10465  expghmap  14686  txdis1cn  15072