Theorem 2falsed 375

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

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

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 206

This theorem is referenced by:  pm5.21ni  376  bianfd  533  sbcel12  4410  sbcne12  4414  sbcel2  4417  sbcbr  5205  csbxp  5779  smoord  8390  tfr2b  8421  axrepnd  10623  hasheq0  14360  m1exp1  16358  sadcadd  16438  stdbdxmet  24442  iccpnfcnv  24887  cxple2  26649  mirbtwnhl  28502  eupth2lem1  30046  ifnebib  32358  isoun  32499  1smat1  33410  xrge0iifcnv  33539  sgn0bi  34172  signswch  34198  fmlafvel  35000  fz0n  35330  hfext  35784  unccur  37081  ntrneiel2  43519  ntrneik4w  43533  eliin2f  44473