Theorem 2falsed 379

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 268	. 2 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
4	3	con4bid 320	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.21ni  380  bianfd  544  sbcel12  4372  sbcne12  4376  sbcel2  4379  sbcbr  5164  csbxp  5757  smoord  8401  tfr2b  8432  ordfin  9259  axrepnd  10706  hasheq0  14534  sgn0bi  15285  m1exp1  16575  sadcadd  16657  isfieldidl  21570  stdbdxmet  24864  iccpnfcnv  25295  cxple2  27055  mirbtwnhl  29182  eupth2lem1  30849  ifnebib  33217  isoun  33366  domnprodeq0  33910  1smat1  34506  xrge0iifcnv  34635  signswch  35260  ecscottd  35844  kard0b  35927  fmlafvel  36317  fz0n  36674  hfext  37112  unccur  38718  ntrneiel2  45278  ntrneik4w  45292  eliin2f  46324