Theorem mpbiran 930

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  932  unssdif  3357  unssin  3361  inssun  3362  invdif  3364  pwpwab  3953  exmidexmid  4175  opabm  4258  regexmidlem1  4510  elirr  4518  en2lp  4531  wessep  4555  peano5  4575  relop  4754  ssrnres  5046  funopab  5223  funcnv2  5248  funcnveq  5251  fnres  5304  idref  5725  rnoprab  5925  elixp  6671  djuf1olem  7018  lbfzo0  10116  txdis1cn  12918