Theorem mpbiran 946

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  948  unssdif  3439  unssin  3443  inssun  3444  invdif  3446  pwpwab  4053  exmidexmid  4280  opabm  4369  regexmidlem1  4625  elirr  4633  en2lp  4646  wessep  4670  peano5  4690  relop  4872  ssrnres  5171  funopab  5353  funcnv2  5381  funcnveq  5384  fnres  5440  idref  5886  rnoprab  6093  elixp  6860  djuf1olem  7228  lbfzo0  10389  expghmap  14579  txdis1cn  14960