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  4351  sbcne12  4355  sbcel2  4358  sbcbr  5140  csbxp  5732  smoord  8305  tfr2b  8335  ordfin  9150  axrepnd  10517  hasheq0  14325  m1exp1  16345  sadcadd  16427  stdbdxmet  24480  iccpnfcnv  24911  cxple2  26661  mirbtwnhl  28748  eupth2lem1  30288  ifnebib  32619  isoun  32775  sgn0bi  32913  domnprodeq0  33337  1smat1  33948  xrge0iifcnv  34077  signswch  34705  fmlafvel  35567  fz0n  35913  hfext  36365  unccur  37924  ntrneiel2  44513  ntrneik4w  44527  eliin2f  45534