Theorem 2falsed 376

Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.) (Proof shortened by Wolf Lammen, 11-Apr-2024.)

Hypotheses

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

Assertion

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

Proof of Theorem 2falsed

Step	Hyp	Ref	Expression
1		2falsed.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2		2falsed.2	. . 3 ⊢ (𝜑 → ¬ 𝜒)
3	1, 2	2thd 265	. 2 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
4	3	con4bid 317	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

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

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 207

This theorem is referenced by:  pm5.21ni  377  bianfd  534  sbcel12  4352  sbcne12  4356  sbcel2  4359  sbcbr  5141  csbxp  5725  smoord  8298  tfr2b  8328  ordfin  9143  axrepnd  10508  hasheq0  14316  m1exp1  16336  sadcadd  16418  stdbdxmet  24490  iccpnfcnv  24921  cxple2  26674  mirbtwnhl  28762  eupth2lem1  30303  ifnebib  32634  isoun  32790  sgn0bi  32928  domnprodeq0  33352  1smat1  33964  xrge0iifcnv  34093  signswch  34721  fmlafvel  35583  fz0n  35929  hfext  36381  unccur  37938  ntrneiel2  44531  ntrneik4w  44545  eliin2f  45552