Theorem mpbiran 946

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  948  unssdif  3440  unssin  3444  inssun  3445  invdif  3447  pwpwab  4056  exmidexmid  4284  opabm  4373  regexmidlem1  4629  elirr  4637  en2lp  4650  wessep  4674  peano5  4694  relop  4878  ssrnres  5177  funopab  5359  funcnv2  5387  funcnveq  5390  fnres  5446  idref  5892  rnoprab  6099  elixp  6869  djuf1olem  7243  lbfzo0  10410  expghmap  14611  txdis1cn  14992