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  4365  sbcne12  4369  sbcel2  4372  sbcbr  5155  csbxp  5733  smoord  8307  tfr2b  8337  ordfin  9152  axrepnd  10517  hasheq0  14298  m1exp1  16315  sadcadd  16397  stdbdxmet  24471  iccpnfcnv  24910  cxple2  26674  mirbtwnhl  28764  eupth2lem1  30305  ifnebib  32635  isoun  32791  sgn0bi  32931  domnprodeq0  33369  1smat1  33981  xrge0iifcnv  34110  signswch  34738  fmlafvel  35598  fz0n  35944  hfext  36396  unccur  37848  ntrneiel2  44436  ntrneik4w  44450  eliin2f  45457