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  4368  sbcne12  4372  sbcel2  4375  sbcbr  5160  csbxp  5751  smoord  8376  tfr2b  8407  ordfin  9234  axrepnd  10682  hasheq0  14510  sgn0bi  15261  m1exp1  16551  sadcadd  16633  isfieldidl  21545  stdbdxmet  24839  iccpnfcnv  25270  cxple2  27030  mirbtwnhl  29157  eupth2lem1  30824  ifnebib  33192  isoun  33342  domnprodeq0  33886  1smat1  34482  xrge0iifcnv  34611  signswch  35236  kard0b  35883  fmlafvel  36236  fz0n  36588  hfext  37026  unccur  38619  ntrneiel2  45179  ntrneik4w  45193  eliin2f  46212