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

Theorem pm2.21d 110
Description: A contradiction implies anything. Deduction associated with 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 26 . 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  357  pm5.14  902  ecase2d  957  prlem1  979  sbc2or  3287  sbcimdv  3340  eq0rdv  3780  csbprc  3781  rzal  3882  reusv2lem2  4618  poirr2  5242  sofld  5302  dfwe2  6634  tfindsg  6713  findsg  6746  omopth2  7310  swoord2  7418  unxpdomlem3  7803  suc11reg  8149  wemapwe  8227  r111  8271  r1pwss  8280  cflim2  8718  axunndlem1  9045  axunnd  9046  axpowndlem3  9049  axpownd  9051  axregndlem1  9052  axregndlem2  9053  axinfndlem1  9055  axinfnd  9056  axacndlem1  9057  axacndlem2  9058  axacndlem3  9059  axacndlem4  9060  axacndlem5  9061  axacnd  9062  fpwwe2lem13  9092  gchpwdom  9120  winalim2  9146  ltapr  9495  prodgt0  10477  squeeze0  10536  nnsub  10675  nn0sub  10948  elnnz  10975  nn0lt10b  11026  indstr2  11265  uzsupss  11284  nn01to3  11285  xrltnsym  11464  xrlttr  11467  qbtwnxr  11521  xltnegi  11537  xmullem  11578  xlemul1a  11602  xrsupsslem  11620  xrinfmsslem  11621  xrub  11625  xrsup0  11637  xrinf0  11651  xrinfm0OLD  11655  reltxrnmnf  11660  ixxdisj  11678  icodisj  11785  fzm1  11902  facdiv  12503  hasheqf1oi  12565  relexpfld  13160  relexpuzrel  13163  climuni  13664  rlimno1  13765  sqrt2irr  14349  prmdvdsexpr  14717  prmfac1  14719  ramlb  15025  ram0  15028  prmgaplem6  15074  prmlem1  15127  prmlem2  15139  pospo  16267  symgbas  17069  efgredlemc  17443  efgred  17446  psrvscafval  18662  prmirred  19114  fvmptnn04ifa  19922  fvmptnn04ifb  19923  fvmptnn04ifc  19924  fvmptnn04ifd  19925  chfacfscmulgsum  19932  chfacfpmmulgsum  19936  0top  20047  pnfnei  20284  mnfnei  20285  cmpfi  20471  1stccnp  20525  filcon  20946  ivthlem2  22451  ivthlem3  22452  ovolicc2lem3  22520  itg1addlem4  22705  itg2seq  22748  dvcnvlem  22976  lhop2  23015  bpos1  24259  lgsdir2lem2  24300  lgsqrlem2  24318  lgseisenlem2  24326  pntlem3  24495  ostth3  24524  tgcgr4  24624  axlowdimlem15  25034  uvtxisvtx  25266  uvtx01vtx  25268  wlkv0  25536  1to2vfriswmgra  25782  n4cyclfrgra  25794  frgranbnb  25796  frgrawopreg  25825  frgraregord013  25894  ifeqeqx  28206  erdszelem4  29965  erdszelem8  29969  finminlem  31022  nn0prpwlem  31026  nn0prpw  31027  ordcmp  31155  iooelexlt  31809  relowlssretop  31810  smprngopr  32329  prtlem14  32490  atltcvr  33044  dihord6apre  34868  dihord6b  34872  jm2.23  35895  sdrgacs  36111  rp-fakeimass  36200  relexpmulg  36346  rzalf  37377  icceuelpart  38787  iccpartnel  38789  evenprm2  38879  stgoldbwt  38914  bgoldbwt  38915  sgoldbalt  38919  nbusgrvtxm1  39502  1wlkv0  39829  ztprmneprm  40400
  Copyright terms: Public domain W3C validator