Theorem mpbiran 949

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  951  unssdif  3456  unssin  3460  inssun  3461  invdif  3463  pwpwab  4079  exmidexmid  4309  opabm  4399  regexmidlem1  4655  elirr  4663  en2lp  4676  wessep  4700  peano5  4720  relop  4905  ssrnres  5205  funopab  5387  funcnv2  5416  funcnveq  5419  fnres  5475  idref  5929  rnoprab  6136  elixp  6940  djuf1olem  7344  lbfzo0  10519  expghmap  14755  txdis1cn  15143