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

Theorem pm2.21i 131
 Description: A contradiction implies anything. Inference associated with pm2.21 108. (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 130 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4 This theorem is referenced by:  pm2.24ii  132  pm2.21dd  174  pm3.2ni  854  falim  1409  nfnth  1628  axc5sp1  2253  rex0  3799  0ss  3814  abf  3819  r19.2zb  3919  ral0  3934  rabsnifsb  4098  snsssn  4198  int0  4300  axnulALT  4579  axc16b  4644  dtrucor  4685  bropopvvv  6880  tfrlem16  7081  omordi  7234  nnmordi  7299  omabs  7315  omsmolem  7321  0er  7365  pssnn  7758  fiint  7817  cantnfle  8111  cantnfleOLD  8141  r1sdom  8213  alephordi  8476  axdc3lem2  8852  canthp1  9053  elnnnn0b  10865  xltnegi  11444  xmulasslem2  11503  xrinfm0  11557  elixx3g  11571  elfz2  11708  om2uzlti  12061  hashf1lem2  12505  sum0  13543  fsum2dlem  13585  prod0  13750  fprod2dlem  13784  exprmfct  14251  4sqlem18  14480  vdwap0  14494  ram0  14540  prmlem1a  14592  prmlem2  14605  xpsfrnel2  14962  0catg  15084  alexsub  20545  0met  20869  vitali  22022  plyeq0  22608  jensen  23318  ppiublem1  23477  ppiublem2  23478  lgsdir2lem3  23600  rpvmasum  23711  usgraedgprv  24376  4cycl4dv  24667  clwwlknprop  24772  2wlkonot3v  24875  2spthonot3v  24876  frgrareggt1  25116  isarchi  27726  sibf0  28276  sgn3da  28480  sgnnbi  28484  sgnpbi  28485  signstfvneq0  28529  sltsolem1  29428  bisym1  29884  unqsym1  29890  amosym1  29891  subsym1  29892  areaquad  31184  iblempty  31764  fveqvfvv  32209  ndmaovcl  32288  bnj98  33925  bj-godellob  34193  bj-axc16b  34384  bj-dtrucor  34386 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
 Copyright terms: Public domain W3C validator