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 114
Description: A contradiction implies anything. Inference associated with pm2.21 118. Its associated inference is pm2.24ii 115. (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 111 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  115  notnotri  124  pm2.21dd  184  pm3.2ni  894  falim  1488  nfnthOLD  1726  rex0  3893  0ss  3923  r19.2zb  4012  ral0  4027  rabsnifsb  4200  snsssn  4307  int0OLD  4420  axnulALT  4709  axc16b  4779  dtrucor  4822  elfv2ex  6124  brfvopab  6576  el2mpt2csbcl  7114  bropopvvv  7119  bropfvvvv  7121  tfrlem16  7353  omordi  7510  nnmordi  7575  omabs  7591  omsmolem  7597  0er  7644  0erOLD  7645  pssnn  8040  fiint  8099  cantnfle  8428  r1sdom  8497  alephordi  8757  axdc3lem2  9133  canthp1  9332  elnnnn0b  11184  xltnegi  11880  xmulasslem2  11941  xrinf0  11995  elixx3g  12015  elfz2  12159  om2uzlti  12566  hashf1lem2  13049  sum0  14245  fsum2dlem  14289  prod0  14458  fprod2dlem  14495  zeneo  14847  nn0enne  14878  exprmfct  15200  prm23lt5  15303  4sqlem18  15450  vdwap0  15464  ram0  15510  prmlem1a  15597  prmlem2  15611  xpsfrnel2  15994  0catg  16117  dfgrp2e  17217  alexsub  21601  0met  21922  vitali  23105  plyeq0  23688  jensen  24432  ppiublem1  24644  ppiublem2  24645  lgsdir2lem3  24769  gausslemma2dlem0i  24806  2lgs  24849  2lgsoddprmlem3  24856  rpvmasum  24932  usgraedgprv  25671  4cycl4dv  25961  clwwlknprop  26066  2wlkonot3v  26168  2spthonot3v  26169  frgrareggt1  26409  topnfbey  26483  isarchi  28873  sibf0  29529  sgn3da  29736  sgnnbi  29740  sgnpbi  29741  signstfvneq0  29781  bnj98  29997  sltsolem1  30873  bisym1  31394  unqsym1  31400  amosym1  31401  subsym1  31402  bj-godellob  31569  bj-axc16b  31792  bj-dtrucor  31794  poimirlem30  32405  axc5sp1  33022  areaquad  36617  fiiuncl  38055  iblempty  38654  vonhoire  39360  fveqvfvv  39650  ndmaovcl  39730  prmdvdsfmtnof1lem2  39833  31prm  39848  lighneallem3  39860  sgoldbaltlem1  39999  bgoldbtbndlem1  40019  xnn0xadd0  40210  vtxdg0v  40683  wlkbProp  40812  0enwwlksnge1  41055  wwlks2onv  41153  rusgr0edg  41171  av-frgrareggt1  41542
  Copyright terms: Public domain W3C validator