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  4386  sbcne12  4390  sbcel2  4393  sbcbr  5174  csbxp  5754  smoord  8379  tfr2b  8410  axrepnd  10608  hasheq0  14381  m1exp1  16395  sadcadd  16477  stdbdxmet  24454  iccpnfcnv  24893  cxple2  26658  mirbtwnhl  28659  eupth2lem1  30199  ifnebib  32530  isoun  32679  sgn0bi  32819  1smat1  33835  xrge0iifcnv  33964  signswch  34593  fmlafvel  35407  fz0n  35748  hfext  36201  unccur  37627  ntrneiel2  44110  ntrneik4w  44124  eliin2f  45128