Theorem mpbiran 846

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  848  unssdif  3166  unssin  3170  inssun  3171  invdif  3173  0pss  3259  pssv  3261  opabm  4008  regexmidlem1  4218  elirr  4224  en2lp  4232  peano5  4264  relop  4429  ssrnres  4706  funopab  4878  funcnv2  4902  funcnveq  4905  fnres  4958  idref  5339  rnoprab  5529  lbfzo0  8807  peano5setOLD  9400