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  4369  sbcne12  4373  sbcel2  4376  sbcbr  5160  csbxp  5752  smoord  8357  tfr2b  8388  ordfin  9215  axrepnd  10660  hasheq0  14487  sgn0bi  15236  m1exp1  16526  sadcadd  16608  isfieldidl  21520  stdbdxmet  24814  iccpnfcnv  25245  cxple2  27007  mirbtwnhl  29134  eupth2lem1  30801  ifnebib  33127  isoun  33277  domnprodeq0  33822  1smat1  34418  xrge0iifcnv  34547  signswch  35173  kard0b  35800  fmlafvel  36119  fz0n  36465  hfext  36904  unccur  38494  ntrneiel2  45045  ntrneik4w  45059  eliin2f  46062