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

Theorem pm2.21d 110
Description: A contradiction implies anything. Deduction from pm2.21 112. (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 27 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 109 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.21ddALT  111  pm2.21  112  2falsed  353  pm5.14  895  ecase2d  949  prlem1  971  sbc2or  3309  sbcimdv  3362  eq0rdv  3798  csbprc  3799  rzal  3900  reusv2lem2  4624  poirr2  5241  sofld  5301  dfwe2  6620  tfindsg  6699  findsg  6732  omopth2  7291  swoord2  7399  unxpdomlem3  7782  suc11reg  8128  wemapwe  8205  r111  8249  r1pwss  8258  cflim2  8695  axunndlem1  9022  axunnd  9023  axpowndlem3  9026  axpownd  9028  axregndlem1  9029  axregndlem2  9030  axinfndlem1  9032  axinfnd  9033  axacndlem1  9034  axacndlem2  9035  axacndlem3  9036  axacndlem4  9037  axacndlem5  9038  axacnd  9039  fpwwe2lem13  9069  gchpwdom  9097  winalim2  9123  ltapr  9472  prodgt0  10452  squeeze0  10511  nnsub  10650  nn0sub  10922  elnnz  10949  nn0lt10b  11000  indstr2  11239  uzsupss  11258  nn01to3  11259  xrltnsym  11438  xrlttr  11441  qbtwnxr  11495  xltnegi  11511  xmullem  11552  xlemul1a  11576  xrsupsslem  11594  xrinfmsslem  11595  xrub  11599  xrsup0  11611  xrinf0  11625  xrinfm0OLD  11629  reltxrnmnf  11634  ixxdisj  11652  icodisj  11759  fzm1  11876  facdiv  12473  hasheqf1oi  12535  relexpfld  13106  relexpuzrel  13109  climuni  13609  rlimno1  13710  sqrt2irr  14294  prmdvdsexpr  14662  prmfac1  14664  ramlb  14970  ram0  14973  prmgaplem6  15019  prmlem1  15072  prmlem2  15084  pospo  16212  symgbas  17014  efgredlemc  17388  efgred  17391  psrvscafval  18607  prmirred  19058  fvmptnn04ifa  19866  fvmptnn04ifb  19867  fvmptnn04ifc  19868  fvmptnn04ifd  19869  chfacfscmulgsum  19876  chfacfpmmulgsum  19880  0top  19991  pnfnei  20228  mnfnei  20229  cmpfi  20415  1stccnp  20469  filcon  20890  ivthlem2  22395  ivthlem3  22396  ovolicc2lem3  22464  itg1addlem4  22649  itg2seq  22692  dvcnvlem  22920  lhop2  22959  bpos1  24203  lgsdir2lem2  24244  lgsqrlem2  24262  lgseisenlem2  24270  pntlem3  24439  ostth3  24468  tgcgr4  24568  axlowdimlem15  24978  uvtxisvtx  25210  uvtx01vtx  25212  wlkv0  25480  1to2vfriswmgra  25726  n4cyclfrgra  25738  frgranbnb  25740  frgrawopreg  25769  frgraregord013  25838  ifeqeqx  28154  erdszelem4  29919  erdszelem8  29923  finminlem  30973  nn0prpwlem  30977  nn0prpw  30978  ordcmp  31106  iooelexlt  31712  relowlssretop  31713  smprngopr  32205  prtlem14  32370  atltcvr  32925  dihord6apre  34749  dihord6b  34753  jm2.23  35777  sdrgacs  35993  rp-fakeimass  36082  relexpmulg  36168  rzalf  37205  icceuelpart  38468  iccpartnel  38470  evenprm2  38560  stgoldbwt  38595  bgoldbwt  38596  sgoldbalt  38600  ztprmneprm  39434
  Copyright terms: Public domain W3C validator