Theorem mpbiran 924

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.)

Hypotheses

Ref	Expression
mpbiran.1	⊢ 𝜓
mpbiran.2	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbiran	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem mpbiran

Step	Hyp	Ref	Expression
1		mpbiran.2	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		mpbiran.1	. . 3 ⊢ 𝜓
3	2	biantrur 301	. 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒))
4	1, 3	bitr4i 186	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbir2an  926  unssdif  3306  unssin  3310  inssun  3311  invdif  3313  pwpwab  3895  exmidexmid  4115  opabm  4197  regexmidlem1  4443  elirr  4451  en2lp  4464  wessep  4487  peano5  4507  relop  4684  ssrnres  4976  funopab  5153  funcnv2  5178  funcnveq  5181  fnres  5234  idref  5651  rnoprab  5847  elixp  6592  djuf1olem  6931  lbfzo0  9951  txdis1cn  12436