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 264	. 2 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
4	3	con4bid 316	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  pm5.21ni  378  bianfd  534  sbcel12  4339  sbcne12  4343  sbcel2  4346  sbcbr  5125  csbxp  5676  smoord  8167  tfr2b  8198  axrepnd  10281  hasheq0  14006  m1exp1  16013  sadcadd  16093  stdbdxmet  23577  iccpnfcnv  24013  cxple2  25757  mirbtwnhl  26945  eupth2lem1  28483  isoun  30936  1smat1  31656  xrge0iifcnv  31785  sgn0bi  32414  signswch  32440  fmlafvel  33247  fz0n  33602  hfext  34412  unccur  35687  ntrneiel2  41585  ntrneik4w  41599  eliin2f  42543