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

Theorem pm2.21d 98
Description: A contradiction implies anything. Deduction from pm2.21 100. (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 22 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 97 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21dd  99  pm2.21  100  2falsed  340  pm5.14  856  ecase2d  906  prlem1  928  sbc2or  3001  eq0rdv  3491  rzal  3557  reusv2lem2  4538  dfwe2  4575  tfindsg  4653  findsg  4685  poirr2  5069  sofld  5123  omopth2  6584  swoord2  6692  unxpdomlem3  7071  suc11reg  7322  wemapwe  7402  r111  7449  r1pwss  7458  cflim2  7891  axunndlem1  8219  axunnd  8220  axpowndlem3  8223  axpownd  8225  axregndlem1  8226  axregndlem2  8227  axinfndlem1  8229  axinfnd  8230  axacndlem1  8231  axacndlem2  8232  axacndlem3  8233  axacndlem4  8234  axacndlem5  8235  axacnd  8236  fpwwe2lem13  8266  gchpwdom  8298  winalim2  8320  ltapr  8671  prodgt0  9603  squeeze0  9661  nnsub  9786  nn0sub  10016  elnnz  10036  indstr2  10298  uzsupss  10312  xrltnsym  10473  xrlttr  10476  qbtwnxr  10529  xltnegi  10545  xmullem  10586  xlemul1a  10610  xrsupsslem  10627  xrinfmsslem  10628  xrub  10632  xrsup0  10644  xrinfm0  10657  ixxdisj  10673  icodisj  10763  facdiv  11302  climuni  12028  rlimno1  12129  sqr2irr  12529  prmdvdsexpr  12797  prmfac1  12799  ramlb  13068  ram0  13071  prmlem1  13111  prmlem2  13123  pospo  14109  symgbas  14774  efgredlemc  15056  efgred  15059  psrvscafval  16137  prmirred  16450  0top  16723  pnfnei  16952  mnfnei  16953  cmpfi  17137  1stccnp  17190  filcon  17580  nmoleub2lem3  18598  ivthlem2  18814  ivthlem3  18815  ovolicc2lem3  18880  itg1addlem4  19056  itg2seq  19099  dvcnvlem  19325  lhop2  19364  bpos1  20524  lgsdir2lem2  20565  lgsqrlem2  20583  lgseisenlem2  20591  pntlem3  20760  ostth3  20789  ifeqeqx  23036  erdszelem4  23727  erdszelem8  23731  axlowdimlem15  24586  ordcmp  24888  nbssntrs  26158  finminlem  26242  nn0prpwlem  26249  nn0prpw  26250  smprngopr  26688  prtlem14  26753  jm2.23  27100  sdrgacs  27520  rzalf  27699  uvtxisvtx  28173  uvtx01vtx  28175  1to2vfriswmgra  28195  ax12-2  29176  a12stdy4  29202  lkrpssN  29426  atltcvr  29697  cdleme27a  30629  dihord6apre  31519  dihord6b  31523
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator