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  5760  smoord  8358  tfr2b  8389  ordfin  9214  axrepnd  10607  hasheq0  14431  sgn0bi  15180  m1exp1  16472  sadcadd  16554  isfieldidl  21455  stdbdxmet  24747  iccpnfcnv  25178  cxple2  26942  mirbtwnhl  29039  eupth2lem1  30706  ifnebib  33032  isoun  33182  domnprodeq0  33727  1smat1  34322  xrge0iifcnv  34451  signswch  35077  kard0b  35693  fmlafvel  35972  fz0n  36318  hfext  36771  unccur  38365  ntrneiel2  44934  ntrneik4w  44948  eliin2f  45944