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  3407  unssin  3411  inssun  3412  invdif  3414  pwpwab  4014  exmidexmid  4239  opabm  4325  regexmidlem1  4579  elirr  4587  en2lp  4600  wessep  4624  peano5  4644  relop  4826  ssrnres  5122  funopab  5303  funcnv2  5328  funcnveq  5331  fnres  5386  idref  5815  rnoprab  6018  elixp  6782  djuf1olem  7137  lbfzo0  10286  expghmap  14287  txdis1cn  14668