Theorem mpbiran 943

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  945  unssdif  3412  unssin  3416  inssun  3417  invdif  3419  pwpwab  4021  exmidexmid  4248  opabm  4335  regexmidlem1  4589  elirr  4597  en2lp  4610  wessep  4634  peano5  4654  relop  4836  ssrnres  5134  funopab  5315  funcnv2  5343  funcnveq  5346  fnres  5402  idref  5838  rnoprab  6041  elixp  6805  djuf1olem  7170  lbfzo0  10327  expghmap  14444  txdis1cn  14825