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 )

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  955  unssdif  3466  unssin  3470  inssun  3471  invdif  3473  pwpwab  4095  exmidexmid  4328  opabm  4418  regexmidlem1  4675  elirr  4683  en2lp  4696  wessep  4720  peano5  4740  relop  4925  ssrnres  5225  funopab  5407  funcnv2  5436  funcnveq  5439  fnres  5495  idref  5952  rnoprab  6161  elixp  6977  djuf1olem  7383  lbfzo0  10570  expghmap  14914  txdis1cn  15302