Theorem 2falsed 377

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 317	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  379  bianfd  535  sbcel12  4342  sbcne12  4346  sbcel2  4349  sbcbr  5129  csbxp  5686  smoord  8196  tfr2b  8227  axrepnd  10350  hasheq0  14078  m1exp1  16085  sadcadd  16165  stdbdxmet  23671  iccpnfcnv  24107  cxple2  25852  mirbtwnhl  27041  eupth2lem1  28582  isoun  31034  1smat1  31754  xrge0iifcnv  31883  sgn0bi  32514  signswch  32540  fmlafvel  33347  fz0n  33696  hfext  34485  unccur  35760  ntrneiel2  41696  ntrneik4w  41710  eliin2f  42654