Theorem 2falsed 379

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 268	. 2 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
4	3	con4bid 320	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

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

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 210

This theorem is referenced by:  pm5.21ni  380  bianfd  543  sbcel12  4377  sbcne12  4381  sbcel2  4384  sbcbr  5167  csbxp  5764  smoord  8353  tfr2b  8384  ordfin  9201  axrepnd  10580  hasheq0  14401  sgn0bi  15142  m1exp1  16435  sadcadd  16517  isfieldidl  21367  stdbdxmet  24653  iccpnfcnv  25084  cxple2  26840  mirbtwnhl  28935  eupth2lem1  30547  ifnebib  32873  isoun  33025  domnprodeq0  33577  1smat1  34172  xrge0iifcnv  34301  signswch  34926  kard0b  35550  fmlafvel  35855  fz0n  36201  hfext  36653  unccur  38232  ntrneiel2  44792  ntrneik4w  44806  eliin2f  45802