Theorem mpbiran 949

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  951  unssdif  3460  unssin  3464  inssun  3465  invdif  3467  pwpwab  4084  exmidexmid  4314  opabm  4404  regexmidlem1  4660  elirr  4668  en2lp  4681  wessep  4705  peano5  4725  relop  4910  ssrnres  5210  funopab  5392  funcnv2  5421  funcnveq  5424  fnres  5480  idref  5935  rnoprab  6144  elixp  6953  djuf1olem  7357  lbfzo0  10541  expghmap  14881  txdis1cn  15269