MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21d Structured version   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  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
pm2.21d  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem pm2.21d
StepHypRef Expression
1 pm2.21d.1 . . 3  |-  ( ph  ->  -.  ps )
21a1d 25 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 105 1  |-  ( ph  ->  ( ps  ->  ch ) )
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-2 7  ax-3 8
This theorem is referenced by:  pm2.21ddOLD  107  pm2.21  108  2falsed  351  pm5.14  884  ecase2d  938  prlem1  960  sbc2or  3340  sbcimdv  3400  eq0rdv  3820  csbprc  3821  rzal  3929  reusv2lem2  4649  poirr2  5389  sofld  5453  dfwe2  6595  tfindsg  6673  findsg  6705  omopth2  7230  swoord2  7338  unxpdomlem3  7723  suc11reg  8032  wemapwe  8135  wemapweOLD  8136  r111  8189  r1pwss  8198  cflim2  8639  axunndlem1  8966  axunnd  8967  axpowndlem3  8971  axpowndlem3OLD  8972  axpownd  8974  axregndlem1  8975  axregndlem2  8976  axinfndlem1  8979  axinfnd  8980  axacndlem1  8981  axacndlem2  8982  axacndlem3  8983  axacndlem4  8984  axacndlem5  8985  axacnd  8986  fpwwe2lem13  9016  gchpwdom  9044  winalim2  9070  ltapr  9419  prodgt0  10383  squeeze0  10444  nnsub  10570  nn0sub  10842  elnnz  10870  indstr2  11156  uzsupss  11170  nn01to3  11171  xrltnsym  11339  xrlttr  11342  qbtwnxr  11395  xltnegi  11411  xmullem  11452  xlemul1a  11476  xrsupsslem  11494  xrinfmsslem  11495  xrub  11499  xrsup0  11511  xrinfm0  11524  ixxdisj  11540  icodisj  11641  facdiv  12329  hasheqf1oi  12388  swrd0  12617  climuni  13334  rlimno1  13435  sqrt2irr  13839  prmdvdsexpr  14112  prmfac1  14114  ramlb  14392  ram0  14395  prmlem1  14447  prmlem2  14459  pospo  15456  symgbas  16200  efgredlemc  16559  efgred  16562  psrvscafval  17814  prmirred  18292  prmirredOLD  18295  fvmptnn04ifa  19118  fvmptnn04ifb  19119  fvmptnn04ifc  19120  fvmptnn04ifd  19121  chfacfscmulgsum  19128  chfacfpmmulgsum  19132  0top  19251  pnfnei  19487  mnfnei  19488  cmpfi  19674  1stccnp  19729  filcon  20119  ivthlem2  21599  ivthlem3  21600  ovolicc2lem3  21665  itg1addlem4  21841  itg2seq  21884  dvcnvlem  22112  lhop2  22151  bpos1  23286  lgsdir2lem2  23327  lgsqrlem2  23345  lgseisenlem2  23353  pntlem3  23522  ostth3  23551  axlowdimlem15  23935  uvtxisvtx  24166  uvtx01vtx  24168  wlkv0  24436  1to2vfriswmgra  24682  n4cyclfrgra  24694  frgranbnb  24696  frgrawopreg  24726  frgraregord013  24795  ifeqeqx  27093  erdszelem4  28278  erdszelem8  28282  ordcmp  29489  finminlem  29713  nn0prpwlem  29717  nn0prpw  29718  smprngopr  30052  prtlem14  30219  jm2.23  30542  sdrgacs  30755  rzalf  30970  fourierdlem65  31472  ztprmneprm  32000  atltcvr  34231  dihord6apre  36053  dihord6b  36057
  Copyright terms: Public domain W3C validator