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

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
StepHypRef Expression
1 2falsed.1 . . 3 (𝜑 → ¬ 𝜓)
2 2falsed.2 . . 3 (𝜑 → ¬ 𝜒)
31, 22thd 265 . 2 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
43con4bid 317 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  379  bianfd  536  sbcel12  4369  sbcne12  4373  sbcel2  4376  sbcbr  5161  csbxp  5732  smoord  8312  tfr2b  8343  axrepnd  10531  hasheq0  14264  m1exp1  16259  sadcadd  16339  stdbdxmet  23874  iccpnfcnv  24310  cxple2  26055  mirbtwnhl  27625  eupth2lem1  29165  isoun  31618  1smat1  32388  xrge0iifcnv  32517  sgn0bi  33150  signswch  33176  fmlafvel  33982  fz0n  34306  hfext  34771  unccur  36064  ntrneiel2  42365  ntrneik4w  42379  eliin2f  43321
  Copyright terms: Public domain W3C validator