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  4361  sbcne12  4365  sbcel2  4368  sbcbr  5146  csbxp  5716  smoord  8285  tfr2b  8315  axrepnd  10482  hasheq0  14267  m1exp1  16284  sadcadd  16366  stdbdxmet  24428  iccpnfcnv  24867  cxple2  26631  mirbtwnhl  28656  eupth2lem1  30193  ifnebib  32524  isoun  32678  sgn0bi  32818  1smat1  33812  xrge0iifcnv  33941  signswch  34569  fmlafvel  35417  fz0n  35763  hfext  36216  unccur  37642  ntrneiel2  44118  ntrneik4w  44132  eliin2f  45140