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

Theorem pm2.21d 106
Description: A contradiction implies anything. Deduction from pm2.21 108. (Contributed by NM, 10-Feb-1996.)
Hypothesis
Ref Expression
pm2.21d.1
Assertion
Ref Expression
pm2.21d

Proof of Theorem pm2.21d
StepHypRef Expression
1 pm2.21d.1 . . 3
21a1d 25 . 2
32con4d 105 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.21ddOLD  107  pm2.21  108  2falsed  351  pm5.14  886  ecase2d  940  prlem1  962  sbc2or  3336  sbcimdv  3396  eq0rdv  3820  csbprc  3821  rzal  3931  reusv2lem2  4654  poirr2  5396  sofld  5460  dfwe2  6617  tfindsg  6695  findsg  6727  omopth2  7252  swoord2  7360  unxpdomlem3  7746  suc11reg  8057  wemapwe  8160  wemapweOLD  8161  r111  8214  r1pwss  8223  cflim2  8664  axunndlem1  8991  axunnd  8992  axpowndlem3  8996  axpowndlem3OLD  8997  axpownd  8999  axregndlem1  9000  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem1  9006  axacndlem2  9007  axacndlem3  9008  axacndlem4  9009  axacndlem5  9010  axacnd  9011  fpwwe2lem13  9041  gchpwdom  9069  winalim2  9095  ltapr  9444  prodgt0  10412  squeeze0  10473  nnsub  10599  nn0sub  10871  elnnz  10899  nn0lt10b  10950  indstr2  11189  uzsupss  11203  nn01to3  11204  xrltnsym  11372  xrlttr  11375  qbtwnxr  11428  xltnegi  11444  xmullem  11485  xlemul1a  11509  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  xrsup0  11544  xrinfm0  11557  ixxdisj  11573  icodisj  11674  fzm1  11787  facdiv  12365  hasheqf1oi  12424  swrd0  12658  climuni  13375  rlimno1  13476  sqrt2irr  13982  prmdvdsexpr  14257  prmfac1  14259  ramlb  14537  ram0  14540  prmlem1  14593  prmlem2  14605  pospo  15603  symgbas  16405  efgredlemc  16763  efgred  16766  psrvscafval  18043  prmirred  18525  prmirredOLD  18528  fvmptnn04ifa  19351  fvmptnn04ifb  19352  fvmptnn04ifc  19353  fvmptnn04ifd  19354  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  0top  19485  pnfnei  19721  mnfnei  19722  cmpfi  19908  1stccnp  19963  filcon  20384  ivthlem2  21864  ivthlem3  21865  ovolicc2lem3  21930  itg1addlem4  22106  itg2seq  22149  dvcnvlem  22377  lhop2  22416  bpos1  23558  lgsdir2lem2  23599  lgsqrlem2  23617  lgseisenlem2  23625  pntlem3  23794  ostth3  23823  axlowdimlem15  24259  uvtxisvtx  24490  uvtx01vtx  24492  wlkv0  24760  1to2vfriswmgra  25006  n4cyclfrgra  25018  frgranbnb  25020  frgrawopreg  25049  frgraregord013  25118  ifeqeqx  27419  erdszelem4  28638  erdszelem8  28642  ordcmp  29912  finminlem  30136  nn0prpwlem  30140  nn0prpw  30141  smprngopr  30449  prtlem14  30615  jm2.23  30938  sdrgacs  31150  rzalf  31392  ztprmneprm  32936  atltcvr  35159  dihord6apre  36983  dihord6b  36987  rp-fakeimass  37736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator