Theorem mpbiran 949

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  951  unssdif  3458  unssin  3462  inssun  3463  invdif  3465  pwpwab  4081  exmidexmid  4311  opabm  4401  regexmidlem1  4657  elirr  4665  en2lp  4678  wessep  4702  peano5  4722  relop  4907  ssrnres  5207  funopab  5389  funcnv2  5418  funcnveq  5421  fnres  5477  idref  5931  rnoprab  6138  elixp  6942  djuf1olem  7346  lbfzo0  10526  expghmap  14804  txdis1cn  15192