Theorem mpbiran 925

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 301	. 2 |- ( ch <-> ( ps /\ ch ) )
4	1, 3	bitr4i 186	1 |- ( ph <-> ch )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbir2an  927  unssdif  3342  unssin  3346  inssun  3347  invdif  3349  pwpwab  3936  exmidexmid  4157  opabm  4240  regexmidlem1  4492  elirr  4500  en2lp  4513  wessep  4537  peano5  4557  relop  4736  ssrnres  5028  funopab  5205  funcnv2  5230  funcnveq  5233  fnres  5286  idref  5707  rnoprab  5904  elixp  6650  djuf1olem  6997  lbfzo0  10080  txdis1cn  12678