Theorem 2falsed 376

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

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

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 207

This theorem is referenced by:  pm5.21ni  377  bianfd  534  sbcel12  4364  sbcne12  4368  sbcel2  4371  sbcbr  5150  csbxp  5723  smoord  8295  tfr2b  8325  axrepnd  10507  hasheq0  14288  m1exp1  16305  sadcadd  16387  stdbdxmet  24419  iccpnfcnv  24858  cxple2  26622  mirbtwnhl  28643  eupth2lem1  30180  ifnebib  32511  isoun  32658  sgn0bi  32798  1smat1  33770  xrge0iifcnv  33899  signswch  34528  fmlafvel  35357  fz0n  35703  hfext  36156  unccur  37582  ntrneiel2  44059  ntrneik4w  44073  eliin2f  45082