Theorem mpbiran 948

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  950  unssdif  3442  unssin  3446  inssun  3447  invdif  3449  pwpwab  4058  exmidexmid  4286  opabm  4375  regexmidlem1  4631  elirr  4639  en2lp  4652  wessep  4676  peano5  4696  relop  4880  ssrnres  5179  funopab  5361  funcnv2  5390  funcnveq  5393  fnres  5449  idref  5896  rnoprab  6103  elixp  6873  djuf1olem  7251  lbfzo0  10419  expghmap  14620  txdis1cn  15001