Theorem mpbiran 953

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  955  unssdif  3466  unssin  3470  inssun  3471  invdif  3473  pwpwab  4098  exmidexmid  4331  opabm  4421  regexmidlem1  4678  elirr  4686  en2lp  4699  wessep  4723  peano5  4743  relop  4928  ssrnres  5228  funopab  5410  funcnv2  5439  funcnveq  5442  fnres  5498  idref  5956  rnoprab  6165  elixp  6981  djuf1olem  7387  lbfzo0  10575  expghmap  14925  txdis1cn  15362