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  3316  unssin  3320  inssun  3321  invdif  3323  pwpwab  3908  exmidexmid  4128  opabm  4210  regexmidlem1  4456  elirr  4464  en2lp  4477  wessep  4500  peano5  4520  relop  4697  ssrnres  4989  funopab  5166  funcnv2  5191  funcnveq  5194  fnres  5247  idref  5666  rnoprab  5862  elixp  6607  djuf1olem  6946  lbfzo0  9989  txdis1cn  12486