Theorem mpbiran 942

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  944  unssdif  3398  unssin  3402  inssun  3403  invdif  3405  pwpwab  4004  exmidexmid  4229  opabm  4315  regexmidlem1  4569  elirr  4577  en2lp  4590  wessep  4614  peano5  4634  relop  4816  ssrnres  5112  funopab  5293  funcnv2  5318  funcnveq  5321  fnres  5374  idref  5803  rnoprab  6005  elixp  6764  djuf1olem  7117  lbfzo0  10254  expghmap  14139  txdis1cn  14490