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  3455  unssin  3459  inssun  3460  invdif  3462  pwpwab  4078  exmidexmid  4308  opabm  4398  regexmidlem1  4654  elirr  4662  en2lp  4675  wessep  4699  peano5  4719  relop  4904  ssrnres  5204  funopab  5386  funcnv2  5415  funcnveq  5418  fnres  5474  idref  5928  rnoprab  6135  elixp  6939  djuf1olem  7343  lbfzo0  10515  expghmap  14742  txdis1cn  15130