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  3320  sbcimdv  3380  eq0rdv  3802  csbprc  3803  rzal  3912  reusv2lem2  4635  poirr2  5377  sofld  5441  dfwe2  6598  tfindsg  6676  findsg  6708  omopth2  7231  swoord2  7339  unxpdomlem3  7724  suc11reg  8034  wemapwe  8137  wemapweOLD  8138  r111  8191  r1pwss  8200  cflim2  8641  axunndlem1  8968  axunnd  8969  axpowndlem3  8973  axpowndlem3OLD  8974  axpownd  8976  axregndlem1  8977  axregndlem2  8978  axinfndlem1  8981  axinfnd  8982  axacndlem1  8983  axacndlem2  8984  axacndlem3  8985  axacndlem4  8986  axacndlem5  8987  axacnd  8988  fpwwe2lem13  9018  gchpwdom  9046  winalim2  9072  ltapr  9421  prodgt0  10388  squeeze0  10449  nnsub  10575  nn0sub  10847  elnnz  10875  nn0lt10b  10927  indstr2  11164  uzsupss  11178  nn01to3  11179  xrltnsym  11347  xrlttr  11350  qbtwnxr  11403  xltnegi  11419  xmullem  11460  xlemul1a  11484  xrsupsslem  11502  xrinfmsslem  11503  xrub  11507  xrsup0  11519  xrinfm0  11532  ixxdisj  11548  icodisj  11649  facdiv  12339  hasheqf1oi  12398  swrd0  12632  climuni  13349  rlimno1  13450  sqrt2irr  13854  prmdvdsexpr  14129  prmfac1  14131  ramlb  14409  ram0  14412  prmlem1  14465  prmlem2  14477  pospo  15472  symgbas  16274  efgredlemc  16632  efgred  16635  psrvscafval  17911  prmirred  18392  prmirredOLD  18395  fvmptnn04ifa  19218  fvmptnn04ifb  19219  fvmptnn04ifc  19220  fvmptnn04ifd  19221  chfacfscmulgsum  19228  chfacfpmmulgsum  19232  0top  19351  pnfnei  19587  mnfnei  19588  cmpfi  19774  1stccnp  19829  filcon  20250  ivthlem2  21730  ivthlem3  21731  ovolicc2lem3  21796  itg1addlem4  21972  itg2seq  22015  dvcnvlem  22243  lhop2  22282  bpos1  23423  lgsdir2lem2  23464  lgsqrlem2  23482  lgseisenlem2  23490  pntlem3  23659  ostth3  23688  axlowdimlem15  24124  uvtxisvtx  24355  uvtx01vtx  24357  wlkv0  24625  1to2vfriswmgra  24871  n4cyclfrgra  24883  frgranbnb  24885  frgrawopreg  24914  frgraregord013  24983  ifeqeqx  27284  erdszelem4  28504  erdszelem8  28508  ordcmp  29880  finminlem  30104  nn0prpwlem  30108  nn0prpw  30109  smprngopr  30417  prtlem14  30583  jm2.23  30906  sdrgacs  31119  rzalf  31339  ztprmneprm  32644  atltcvr  34861  dihord6apre  36685  dihord6b  36689  rp-fakeimass  37401
  Copyright terms: Public domain W3C validator