Theorem mpbiran 946

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  948  unssdif  3439  unssin  3443  inssun  3444  invdif  3446  pwpwab  4052  exmidexmid  4279  opabm  4368  regexmidlem1  4624  elirr  4632  en2lp  4645  wessep  4669  peano5  4689  relop  4871  ssrnres  5170  funopab  5352  funcnv2  5380  funcnveq  5383  fnres  5439  idref  5879  rnoprab  6086  elixp  6850  djuf1olem  7216  lbfzo0  10377  expghmap  14565  txdis1cn  14946