Theorem 2falsed 379

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

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

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 210

This theorem is referenced by:  pm5.21ni  380  bianfd  543  sbcel12  4368  sbcne12  4372  sbcel2  4375  sbcbr  5160  csbxp  5753  smoord  8340  tfr2b  8371  ordfin  9188  axrepnd  10567  hasheq0  14390  sgn0bi  15130  m1exp1  16424  sadcadd  16506  stdbdxmet  24633  iccpnfcnv  25064  cxple2  26820  mirbtwnhl  28911  eupth2lem1  30478  ifnebib  32805  isoun  32959  domnprodeq0  33512  1smat1  34111  xrge0iifcnv  34240  signswch  34865  fmlafvel  35748  fz0n  36094  hfext  36546  unccur  38114  ntrneiel2  44674  ntrneik4w  44688  eliin2f  45680