Theorem mpbiran 948

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  950  unssdif  3442  unssin  3446  inssun  3447  invdif  3449  pwpwab  4058  exmidexmid  4286  opabm  4375  regexmidlem1  4631  elirr  4639  en2lp  4652  wessep  4676  peano5  4696  relop  4880  ssrnres  5179  funopab  5361  funcnv2  5390  funcnveq  5393  fnres  5449  idref  5897  rnoprab  6104  elixp  6874  djuf1olem  7252  lbfzo0  10420  expghmap  14624  txdis1cn  15005