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  4363  sbcne12  4367  sbcel2  4370  sbcbr  5153  csbxp  5725  smoord  8297  tfr2b  8327  ordfin  9140  axrepnd  10505  hasheq0  14286  m1exp1  16303  sadcadd  16385  stdbdxmet  24459  iccpnfcnv  24898  cxple2  26662  mirbtwnhl  28752  eupth2lem1  30293  ifnebib  32624  isoun  32781  sgn0bi  32921  domnprodeq0  33358  1smat1  33961  xrge0iifcnv  34090  signswch  34718  fmlafvel  35579  fz0n  35925  hfext  36377  unccur  37800  ntrneiel2  44323  ntrneik4w  44337  eliin2f  45344