Theorem mpbiran 942

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  944  unssdif  3394  unssin  3398  inssun  3399  invdif  3401  pwpwab  4000  exmidexmid  4225  opabm  4309  regexmidlem1  4563  elirr  4571  en2lp  4584  wessep  4608  peano5  4628  relop  4808  ssrnres  5104  funopab  5285  funcnv2  5310  funcnveq  5313  fnres  5366  idref  5795  rnoprab  5997  elixp  6754  djuf1olem  7106  lbfzo0  10242  txdis1cn  14427