Theorem 2falsed 377

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208

This theorem is referenced by:  pm5.21ni  378  bianfd  539  sbcel12  4346  sbcne12  4350  sbcel2  4353  sbcbr  5134  csbxp  5726  smoord  8302  tfr2b  8332  ordfin  9147  axrepnd  10515  hasheq0  14323  m1exp1  16343  sadcadd  16425  stdbdxmet  24505  iccpnfcnv  24936  cxple2  26686  mirbtwnhl  28773  eupth2lem1  30313  ifnebib  32644  isoun  32801  sgn0bi  32939  domnprodeq0  33364  1smat1  33995  xrge0iifcnv  34124  signswch  34752  fmlafvel  35620  fz0n  35966  hfext  36418  unccur  37977  ntrneiel2  44537  ntrneik4w  44551  eliin2f  45558