Theorem 2falsed 376

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 265	. 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  377  bianfd  534  sbcel12  4404  sbcne12  4408  sbcel2  4411  sbcbr  5197  csbxp  5771  smoord  8379  tfr2b  8410  axrepnd  10611  hasheq0  14348  m1exp1  16346  sadcadd  16426  stdbdxmet  24417  iccpnfcnv  24862  cxple2  26624  mirbtwnhl  28477  eupth2lem1  30021  ifnebib  32333  isoun  32475  1smat1  33399  xrge0iifcnv  33528  sgn0bi  34161  signswch  34187  fmlafvel  34989  fz0n  35319  hfext  35773  unccur  37070  ntrneiel2  43510  ntrneik4w  43524  eliin2f  44464

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »