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  4434  sbcne12  4438  sbcel2  4441  sbcbr  5221  csbxp  5799  smoord  8421  tfr2b  8452  axrepnd  10663  hasheq0  14412  m1exp1  16424  sadcadd  16504  stdbdxmet  24549  iccpnfcnv  24994  cxple2  26757  mirbtwnhl  28706  eupth2lem1  30250  ifnebib  32572  isoun  32713  1smat1  33750  xrge0iifcnv  33879  sgn0bi  34512  signswch  34538  fmlafvel  35353  fz0n  35693  hfext  36147  unccur  37563  ntrneiel2  44048  ntrneik4w  44062  eliin2f  45006