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  pm2.21dd  186  pm3.2ni  894  annotanannotOLD  1023  falim  1649  nfnthOLD  1887  rex0  4096  0ss  4127  r19.2zb  4212  ral0  4227  rabsnifsb  4404  snsssn  4516  axnulALT  4934  axc16b  5003  dtrucor  5042  elfv2ex  6387  brfvopab  6868  el2mpt2csbcl  7421  bropopvvv  7427  bropfvvvv  7429  tfrlem16  7663  omordi  7821  nnmordi  7886  omabs  7902  omsmolem  7908  0er  7954  pssnn  8355  fiint  8414  cantnfle  8753  r1sdom  8822  alephordi  9118  axdc3lem2  9496  canthp1  9699  elnnnn0b  11561  xltnegi  12271  xnn0xadd0  12301  xmulasslem2  12336  xrinf0  12392  elixx3g  12412  elfz2  12562  om2uzlti  12979  hashf1lem2  13464  sum0  14682  fsum2dlem  14731  prod0  14902  fprod2dlem  14939  nn0enne  15324  exprmfct  15643  prm23lt5  15746  4sqlem18  15893  vdwap0  15907  ram0  15953  prmlem1a  16040  prmlem2  16054  xpsfrnel2  16453  0catg  16575  dfgrp2e  17676  alexsub  22089  0met  22411  vitali  23621  plyeq0  24208  jensen  24957  ppiublem1  25169  ppiublem2  25170  lgsdir2lem3  25294  gausslemma2dlem0i  25331  2lgs  25374  2lgsoddprmlem3  25381  rpvmasum  25457  vtxdg0v  26625  0enwwlksnge1  27019  rusgr0edg  27143  frgrreggt1  27609  topnfbey  27684  n0lpligALT  27695  isarchi  30093  sibf0  30753  sgn3da  30960  sgnnbi  30964  sgnpbi  30965  signstfvneq0  31006  bnj98  31292  sltsolem1  32180  bisym1  32772  unqsym1  32778  amosym1  32779  subsym1  32780  bj-godellob  32943  bj-axc16b  33150  bj-dtrucor  33152  poimirlem30  33789  axc5sp1  34746  areaquad  38342  fiiuncl  39767  iblempty  40704  vonhoire  41412  fveqvfvv  41749  ndmaovcl  41828  prmdvdsfmtnof1lem2  42049  31prm  42064  lighneallem3  42076  sbgoldbaltlem1  42219  bgoldbtbndlem1  42245  upwlkbprop  42271
  Copyright terms: Public domain W3C validator