MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21dd Structured version   Visualization version   GIF version

Theorem pm2.21dd 186
Description: A contradiction implies anything. Deduction from pm2.21 121. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.)
Hypotheses
Ref Expression
pm2.21dd.1 (𝜑𝜓)
pm2.21dd.2 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
pm2.21dd (𝜑𝜒)

Proof of Theorem pm2.21dd
StepHypRef Expression
1 pm2.21dd.1 . . 3 (𝜑𝜓)
2 pm2.21dd.2 . . 3 (𝜑 → ¬ 𝜓)
31, 2pm2.65i 185 . 2 ¬ 𝜑
43pm2.21i 117 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.21fal  1652  pm2.21ddne  3026  smo11  7613  ackbij1lem16  9258  cfsmolem  9293  domtriomlem  9465  konigthlem  9591  grur1  9843  uzdisj  12619  nn0disj  12662  psgnunilem2  18121  nmoleub2lem3  23133  i1f0  23673  itg2const2  23727  bposlem3  25231  bposlem9  25237  pntpbnd1  25495  fzto1st1  30186  esumpcvgval  30474  sgnmul  30938  sgnmulsgn  30945  sgnmulsgp  30946  signstfvneq0  30983  derangsn  31484  heiborlem8  33942  lkrpssN  34965  cdleme27a  36169  pellfundex  37969  monotoddzzfi  38026  jm2.23  38082  rp-isfinite6  38383  iccpartiltu  41876  iccpartigtl  41877
  Copyright terms: Public domain W3C validator