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  4360  sbcne12  4364  sbcel2  4367  sbcbr  5148  csbxp  5720  smoord  8291  tfr2b  8321  axrepnd  10492  hasheq0  14272  m1exp1  16289  sadcadd  16371  stdbdxmet  24431  iccpnfcnv  24870  cxple2  26634  mirbtwnhl  28659  eupth2lem1  30200  ifnebib  32531  isoun  32687  sgn0bi  32828  1smat1  33838  xrge0iifcnv  33967  signswch  34595  fmlafvel  35450  fz0n  35796  hfext  36248  unccur  37663  ntrneiel2  44203  ntrneik4w  44217  eliin2f  45225