Theorem 2falsed 377

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 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  379  bianfd  536  sbcel12  4409  sbcne12  4413  sbcel2  4416  sbcbr  5204  csbxp  5776  smoord  8365  tfr2b  8396  axrepnd  10589  hasheq0  14323  m1exp1  16319  sadcadd  16399  stdbdxmet  24024  iccpnfcnv  24460  cxple2  26205  mirbtwnhl  27962  eupth2lem1  29502  ifnebib  31812  isoun  31954  1smat1  32815  xrge0iifcnv  32944  sgn0bi  33577  signswch  33603  fmlafvel  34407  fz0n  34731  hfext  35186  unccur  36519  ntrneiel2  42885  ntrneik4w  42899  eliin2f  43841