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  349  pm5.14  884  ecase2d  938  prlem1  960  sbc2or  3333  sbcimdv  3386  eq0rdv  3819  csbprc  3820  rzal  3919  reusv2lem2  4639  poirr2  5379  sofld  5439  dfwe2  6590  tfindsg  6668  findsg  6700  omopth2  7225  swoord2  7333  unxpdomlem3  7719  suc11reg  8027  wemapwe  8130  wemapweOLD  8131  r111  8184  r1pwss  8193  cflim2  8634  axunndlem1  8961  axunnd  8962  axpowndlem3  8965  axpownd  8967  axregndlem1  8968  axregndlem2  8969  axinfndlem1  8972  axinfnd  8973  axacndlem1  8974  axacndlem2  8975  axacndlem3  8976  axacndlem4  8977  axacndlem5  8978  axacnd  8979  fpwwe2lem13  9009  gchpwdom  9037  winalim2  9063  ltapr  9412  prodgt0  10383  squeeze0  10443  nnsub  10570  nn0sub  10842  elnnz  10870  nn0lt10b  10921  indstr2  11161  uzsupss  11175  nn01to3  11176  xrltnsym  11346  xrlttr  11349  qbtwnxr  11402  xltnegi  11418  xmullem  11459  xlemul1a  11483  xrsupsslem  11501  xrinfmsslem  11502  xrub  11506  xrsup0  11518  xrinfm0  11531  ixxdisj  11547  icodisj  11648  fzm1  11762  facdiv  12347  hasheqf1oi  12406  relexpfld  12964  relexpuzrel  12967  climuni  13457  rlimno1  13558  sqrt2irr  14066  prmdvdsexpr  14341  prmfac1  14343  ramlb  14621  ram0  14624  prmlem1  14677  prmlem2  14689  pospo  15802  symgbas  16604  efgredlemc  16962  efgred  16965  psrvscafval  18238  prmirred  18707  fvmptnn04ifa  19518  fvmptnn04ifb  19519  fvmptnn04ifc  19520  fvmptnn04ifd  19521  chfacfscmulgsum  19528  chfacfpmmulgsum  19532  0top  19652  pnfnei  19888  mnfnei  19889  cmpfi  20075  1stccnp  20129  filcon  20550  ivthlem2  22030  ivthlem3  22031  ovolicc2lem3  22096  itg1addlem4  22272  itg2seq  22315  dvcnvlem  22543  lhop2  22582  bpos1  23756  lgsdir2lem2  23797  lgsqrlem2  23815  lgseisenlem2  23823  pntlem3  23992  ostth3  24021  axlowdimlem15  24461  uvtxisvtx  24692  uvtx01vtx  24694  wlkv0  24962  1to2vfriswmgra  25208  n4cyclfrgra  25220  frgranbnb  25222  frgrawopreg  25251  frgraregord013  25320  ifeqeqx  27625  erdszelem4  28902  erdszelem8  28906  ordcmp  30140  finminlem  30376  nn0prpwlem  30380  nn0prpw  30381  smprngopr  30689  prtlem14  30855  jm2.23  31177  sdrgacs  31391  rzalf  31632  ztprmneprm  33190  atltcvr  35556  dihord6apre  37380  dihord6b  37384  rp-fakeimass  38150  relexpmulg  38228
  Copyright terms: Public domain W3C validator