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  4379  sbcne12  4383  sbcel2  4386  sbcbr  5171  csbxp  5767  smoord  8361  tfr2b  8392  ordfin  9210  axrepnd  10597  hasheq0  14419  sgn0bi  15166  m1exp1  16459  sadcadd  16541  isfieldidl  21423  stdbdxmet  24709  iccpnfcnv  25140  cxple2  26899  mirbtwnhl  28994  eupth2lem1  30606  ifnebib  32932  isoun  33084  domnprodeq0  33630  1smat1  34225  xrge0iifcnv  34354  signswch  34980  kard0b  35596  fmlafvel  35898  fz0n  36244  hfext  36696  unccur  38295  ntrneiel2  44853  ntrneik4w  44867  eliin2f  45863