Theorem mpbiran 935

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  937  unssdif  3362  unssin  3366  inssun  3367  invdif  3369  pwpwab  3960  exmidexmid  4182  opabm  4265  regexmidlem1  4517  elirr  4525  en2lp  4538  wessep  4562  peano5  4582  relop  4761  ssrnres  5053  funopab  5233  funcnv2  5258  funcnveq  5261  fnres  5314  idref  5736  rnoprab  5936  elixp  6683  djuf1olem  7030  lbfzo0  10137  txdis1cn  13072