Theorem mpbiran 847

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 287	. 2 |- ( ch <-> ( ps /\ ch ) )
4	1, 3	bitr4i 176	1 |- ( ph <-> ch )

Syntax hints:   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  mpbir2an  849  unssdif  3172  unssin  3176  inssun  3177  invdif  3179  0pss  3265  pssv  3267  opabm  4017  regexmidlem1  4258  elirr  4266  en2lp  4278  wessep  4302  peano5  4321  relop  4486  ssrnres  4763  funopab  4935  funcnv2  4959  funcnveq  4962  fnres  5015  idref  5396  rnoprab  5587  lbfzo0  9037  peano5setOLD  10065