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  3311  unssin  3315  inssun  3316  invdif  3318  pwpwab  3900  exmidexmid  4120  opabm  4202  regexmidlem1  4448  elirr  4456  en2lp  4469  wessep  4492  peano5  4512  relop  4689  ssrnres  4981  funopab  5158  funcnv2  5183  funcnveq  5186  fnres  5239  idref  5658  rnoprab  5854  elixp  6599  djuf1olem  6938  lbfzo0  9958  txdis1cn  12447