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  4377  sbcne12  4381  sbcel2  4384  sbcbr  5165  csbxp  5741  smoord  8337  tfr2b  8367  axrepnd  10554  hasheq0  14335  m1exp1  16353  sadcadd  16435  stdbdxmet  24410  iccpnfcnv  24849  cxple2  26613  mirbtwnhl  28614  eupth2lem1  30154  ifnebib  32485  isoun  32632  sgn0bi  32772  1smat1  33801  xrge0iifcnv  33930  signswch  34559  fmlafvel  35379  fz0n  35725  hfext  36178  unccur  37604  ntrneiel2  44082  ntrneik4w  44096  eliin2f  45105