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  4374  sbcne12  4378  sbcel2  4381  sbcbr  5162  csbxp  5738  smoord  8334  tfr2b  8364  axrepnd  10547  hasheq0  14328  m1exp1  16346  sadcadd  16428  stdbdxmet  24403  iccpnfcnv  24842  cxple2  26606  mirbtwnhl  28607  eupth2lem1  30147  ifnebib  32478  isoun  32625  sgn0bi  32765  1smat1  33794  xrge0iifcnv  33923  signswch  34552  fmlafvel  35372  fz0n  35718  hfext  36171  unccur  37597  ntrneiel2  44075  ntrneik4w  44089  eliin2f  45098