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  3441  unssin  3445  inssun  3446  invdif  3448  pwpwab  4059  exmidexmid  4288  opabm  4377  regexmidlem1  4633  elirr  4641  en2lp  4654  wessep  4678  peano5  4698  relop  4882  ssrnres  5181  funopab  5363  funcnv2  5392  funcnveq  5395  fnres  5451  idref  5902  rnoprab  6109  elixp  6879  djuf1olem  7257  lbfzo0  10425  expghmap  14645  txdis1cn  15031