Theorem mpbiran 892

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 299	. 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒))
4	1, 3	bitr4i 186	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbir2an  894  unssdif  3258  unssin  3262  inssun  3263  invdif  3265  pwpwab  3846  exmidexmid  4060  opabm  4140  regexmidlem1  4386  elirr  4394  en2lp  4407  wessep  4430  peano5  4450  relop  4627  ssrnres  4917  funopab  5094  funcnv2  5119  funcnveq  5122  fnres  5175  idref  5590  rnoprab  5786  elixp  6529  djuf1olem  6853  lbfzo0  9799  txdis1cn  12228