Theorem mpbiran 942

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

Syntax hints:   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbir2an  944  unssdif  3394  unssin  3398  inssun  3399  invdif  3401  pwpwab  4000  exmidexmid  4225  opabm  4311  regexmidlem1  4565  elirr  4573  en2lp  4586  wessep  4610  peano5  4630  relop  4812  ssrnres  5108  funopab  5289  funcnv2  5314  funcnveq  5317  fnres  5370  idref  5799  rnoprab  6001  elixp  6759  djuf1olem  7112  lbfzo0  10248  expghmap  14095  txdis1cn  14446