Theorem mpbiran 942

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  944  unssdif  3395  unssin  3399  inssun  3400  invdif  3402  pwpwab  4001  exmidexmid  4226  opabm  4312  regexmidlem1  4566  elirr  4574  en2lp  4587  wessep  4611  peano5  4631  relop  4813  ssrnres  5109  funopab  5290  funcnv2  5315  funcnveq  5318  fnres  5371  idref  5800  rnoprab  6002  elixp  6761  djuf1olem  7114  lbfzo0  10251  expghmap  14106  txdis1cn  14457