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  4333  opabm  4423  regexmidlem1  4680  elirr  4688  en2lp  4701  wessep  4725  peano5  4745  relop  4930  ssrnres  5230  funopab  5412  funcnv2  5441  funcnveq  5444  fnres  5500  idref  5962  rnoprab  6171  elixp  6987  djuf1olem  7393  lbfzo0  10592  expghmap  14942  txdis1cn  15379