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  535  sbcel12  4373  sbcne12  4377  sbcel2  4380  sbcbr  5165  csbxp  5736  smoord  8316  tfr2b  8347  axrepnd  10539  hasheq0  14273  m1exp1  16269  sadcadd  16349  stdbdxmet  23908  iccpnfcnv  24344  cxple2  26089  mirbtwnhl  27685  eupth2lem1  29225  ifnebib  31535  isoun  31683  1smat1  32474  xrge0iifcnv  32603  sgn0bi  33236  signswch  33262  fmlafvel  34066  fz0n  34389  hfext  34844  unccur  36134  ntrneiel2  42480  ntrneik4w  42494  eliin2f  43436