Theorem mpbiran 929

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  931  unssdif  3352  unssin  3356  inssun  3357  invdif  3359  pwpwab  3947  exmidexmid  4169  opabm  4252  regexmidlem1  4504  elirr  4512  en2lp  4525  wessep  4549  peano5  4569  relop  4748  ssrnres  5040  funopab  5217  funcnv2  5242  funcnveq  5245  fnres  5298  idref  5719  rnoprab  5916  elixp  6662  djuf1olem  7009  lbfzo0  10106  txdis1cn  12819