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 120. (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 116 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  1502  pm2.21ddne  2874  smo11  7406  ackbij1lem16  9001  cfsmolem  9036  domtriomlem  9208  konigthlem  9334  grur1  9586  uzdisj  12354  nn0disj  12396  psgnunilem2  17836  nmoleub2lem3  22823  i1f0  23360  itg2const2  23414  bposlem3  24911  bposlem9  24917  pntpbnd1  25175  fzto1st1  29634  esumpcvgval  29918  sgnmul  30382  sgnmulsgn  30389  sgnmulsgp  30390  signstfvneq0  30426  derangsn  30857  heiborlem8  33246  lkrpssN  33927  cdleme27a  35132  pellfundex  36927  monotoddzzfi  36984  jm2.23  37040  rp-isfinite6  37342  iccpartiltu  40653  iccpartigtl  40654
 Copyright terms: Public domain W3C validator