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  4352  sbcne12  4356  sbcel2  4359  sbcbr  5141  csbxp  5723  smoord  8296  tfr2b  8326  ordfin  9141  axrepnd  10506  hasheq0  14287  m1exp1  16304  sadcadd  16386  stdbdxmet  24458  iccpnfcnv  24889  cxple2  26646  mirbtwnhl  28736  eupth2lem1  30277  ifnebib  32608  isoun  32764  sgn0bi  32904  domnprodeq0  33342  1smat1  33954  xrge0iifcnv  34083  signswch  34711  fmlafvel  35573  fz0n  35919  hfext  36371  unccur  37915  ntrneiel2  44516  ntrneik4w  44530  eliin2f  45537