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  4417  sbcne12  4421  sbcel2  4424  sbcbr  5203  csbxp  5788  smoord  8404  tfr2b  8435  axrepnd  10632  hasheq0  14399  m1exp1  16410  sadcadd  16492  stdbdxmet  24544  iccpnfcnv  24989  cxple2  26754  mirbtwnhl  28703  eupth2lem1  30247  ifnebib  32570  isoun  32717  1smat1  33765  xrge0iifcnv  33894  sgn0bi  34529  signswch  34555  fmlafvel  35370  fz0n  35711  hfext  36165  unccur  37590  ntrneiel2  44076  ntrneik4w  44090  eliin2f  45044