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

Theorem pm2.21i 117
Description: A contradiction implies anything. Inference associated with pm2.21 121. Its associated inference is pm2.24ii 118. (Contributed by NM, 16-Sep-1993.)
Hypothesis
Ref Expression
pm2.21i.1 ¬ 𝜑
Assertion
Ref Expression
pm2.21i (𝜑𝜓)

Proof of Theorem pm2.21i
StepHypRef Expression
1 pm2.21i.1 . . 3 ¬ 𝜑
21a1i 11 . 2 𝜓 → ¬ 𝜑)
32con4i 114 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-3 8
This theorem is referenced by:  pm2.24ii  118  notnotri  129  notnotriALT  130  pm2.21dd  187  pm3.2ni  905  annotanannotOLD  1035  falim  1671  rex0  4138  0ss  4168  r19.2zb  4254  ral0  4269  rabsnifsb  4446  snsssn  4558  axnulALT  4981  dtrucor  5041  axc16b  5058  elfv2ex  6453  brfvopab  6934  el2mpt2csbcl  7486  bropopvvv  7492  bropfvvvv  7494  tfrlem16  7728  omordi  7886  nnmordi  7951  omabs  7967  omsmolem  7973  0er  8019  pssnn  8420  fiint  8479  cantnfle  8818  r1sdom  8887  alephordi  9183  axdc3lem2  9561  canthp1  9764  elnnnn0b  11626  xltnegi  12296  xnn0xadd0  12326  xmulasslem2  12361  xrinf0  12417  elixx3g  12437  elfz2  12587  om2uzlti  13004  hashf1lem2  13489  sum0  14793  fsum2dlem  14840  prod0  15010  fprod2dlem  15047  nn0enne  15430  exprmfct  15749  prm23lt5  15852  4sqlem18  15999  vdwap0  16013  ram0  16059  prmlem1a  16141  prmlem2  16154  xpsfrnel2  16540  0catg  16662  dfgrp2e  17764  alexsub  22177  0met  22499  vitali  23721  plyeq0  24308  jensen  25067  ppiublem1  25279  ppiublem2  25280  lgsdir2lem3  25404  gausslemma2dlem0i  25441  2lgs  25484  2lgsoddprmlem3  25491  rpvmasum  25567  vtxdg0v  26723  0enwwlksnge1  27121  rusgr0edg  27264  frgrreggt1  27778  topnfbey  27853  n0lpligALT  27864  isarchi  30252  sibf0  30912  sgn3da  31120  sgnnbi  31124  sgnpbi  31125  signstfvneq0  31168  bnj98  31454  sltsolem1  32339  bisym1  32926  unqsym1  32932  amosym1  32933  subsym1  32934  bj-godellob  33095  bj-axc16b  33294  bj-dtrucor  33296  poimirlem30  33928  axc5sp1  34944  areaquad  38582  fiiuncl  39989  iblempty  40920  vonhoire  41628  fveqvfvv  41919  ndmaovcl  42053  prmdvdsfmtnof1lem2  42275  31prm  42290  lighneallem3  42302  sbgoldbaltlem1  42445  bgoldbtbndlem1  42471  upwlkbprop  42514
  Copyright terms: Public domain W3C validator