MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2falsed Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 2falsed.1 . . 3 (𝜑 → ¬ 𝜓)
2 2falsed.2 . . 3 (𝜑 → ¬ 𝜒)
31, 22thd 264 . 2 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
43con4bid 316 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
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  378  bianfd  535  sbcel12  4408  sbcne12  4412  sbcel2  4415  sbcbr  5203  csbxp  5775  smoord  8367  tfr2b  8398  axrepnd  10591  hasheq0  14327  m1exp1  16323  sadcadd  16403  stdbdxmet  24244  iccpnfcnv  24684  cxple2  26429  mirbtwnhl  28186  eupth2lem1  29726  ifnebib  32036  isoun  32178  1smat1  33070  xrge0iifcnv  33199  sgn0bi  33832  signswch  33858  fmlafvel  34662  fz0n  34992  hfext  35447  unccur  36774  ntrneiel2  43139  ntrneik4w  43153  eliin2f  44095
  Copyright terms: Public domain W3C validator