Theorem mpbiran 945

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  947  unssdif  3419  unssin  3423  inssun  3424  invdif  3426  pwpwab  4032  exmidexmid  4259  opabm  4348  regexmidlem1  4602  elirr  4610  en2lp  4623  wessep  4647  peano5  4667  relop  4849  ssrnres  5147  funopab  5329  funcnv2  5357  funcnveq  5360  fnres  5416  idref  5853  rnoprab  6058  elixp  6822  djuf1olem  7188  lbfzo0  10349  expghmap  14536  txdis1cn  14917