Theorem 2falsed 378

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

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

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 209

This theorem is referenced by:  pm5.21ni  379  bianfd  542  sbcel12  4364  sbcne12  4368  sbcel2  4371  sbcbr  5154  csbxp  5746  smoord  8331  tfr2b  8362  ordfin  9180  axrepnd  10549  hasheq0  14373  m1exp1  16393  sadcadd  16475  stdbdxmet  24555  iccpnfcnv  24986  cxple2  26739  mirbtwnhl  28826  eupth2lem1  30366  ifnebib  32697  isoun  32854  sgn0bi  32992  domnprodeq0  33421  1smat1  34062  xrge0iifcnv  34191  signswch  34819  fmlafvel  35699  fz0n  36045  hfext  36497  unccur  38066  ntrneiel2  44626  ntrneik4w  44640  eliin2f  45646