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 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  381  bianfd  537  sbcel12  4362  sbcne12  4366  sbcel2  4369  sbcbr  5123  csbxp  5652  smoord  8004  tfr2b  8034  axrepnd  10018  hasheq0  13727  m1exp1  15729  sadcadd  15809  stdbdxmet  23127  iccpnfcnv  23550  cxple2  25282  mirbtwnhl  26468  eupth2lem1  27999  isoun  30439  1smat1  31071  xrge0iifcnv  31178  sgn0bi  31807  signswch  31833  fmlafvel  32634  fz0n  32964  hfext  33646  unccur  34877  ntrneiel2  40443  ntrneik4w  40457  eliin2f  41377