Theorem mpbiran 953

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 )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbir2an  955  unssdif  3466  unssin  3470  inssun  3471  invdif  3473  pwpwab  4100  exmidexmid  4335  opabm  4425  regexmidlem1  4682  elirr  4690  en2lp  4703  wessep  4727  peano5  4747  relop  4932  ssrnres  5233  funopab  5415  funcnv2  5444  funcnveq  5447  fnres  5503  idref  5965  rnoprab  6174  elixp  6991  djuf1olem  7399  lbfzo0  10609  expghmap  15051  txdis1cn  15504