Theorem 2falsed 378

Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.)

Hypotheses

Ref	Expression
2falsed.1	⊢ (𝜑 → ¬ 𝜓)
2falsed.2	⊢ (𝜑 → ¬ 𝜒)

Assertion

Ref	Expression
2falsed	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem 2falsed

Step	Hyp	Ref	Expression
1		2falsed.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2	1	pm2.21d 121	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		2falsed.2	. . 3 ⊢ (𝜑 → ¬ 𝜒)
4	3	pm2.21d 121	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 213	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208

This theorem is referenced by:  pm5.21ni  379  bianfd  535  sbcel12  4284  sbcne12  4288  sbcel2  4291  sbcbr  5021  csbxp  5541  smoord  7859  tfr2b  7889  axrepnd  9867  hasheq0  13579  m1exp1  15565  sadcadd  15645  stdbdxmet  22813  iccpnfcnv  23236  cxple2  24966  mirbtwnhl  26153  eupth2lem1  27690  isoun  30130  1smat1  30689  xrge0iifcnv  30798  sgn0bi  31427  signswch  31453  fmlafvel  32247  fz0n  32577  hfext  33260  unccur  34432  ntrneiel2  39947  ntrneik4w  39961  eliin2f  40936