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  3085  eq0rdv  3577  rzal  3644  reusv2lem2  4639  dfwe2  4676  tfindsg  4754  findsg  4786  poirr2  5170  sofld  5224  omopth2  6724  swoord2  6832  unxpdomlem3  7212  suc11reg  7467  wemapwe  7547  r111  7594  r1pwss  7603  cflim2  8036  axunndlem1  8364  axunnd  8365  axpowndlem3  8368  axpownd  8370  axregndlem1  8371  axregndlem2  8372  axinfndlem1  8374  axinfnd  8375  axacndlem1  8376  axacndlem2  8377  axacndlem3  8378  axacndlem4  8379  axacndlem5  8380  axacnd  8381  fpwwe2lem13  8411  gchpwdom  8443  winalim2  8465  ltapr  8816  prodgt0  9748  squeeze0  9806  nnsub  9931  nn0sub  10163  elnnz  10185  indstr2  10447  uzsupss  10461  xrltnsym  10623  xrlttr  10626  qbtwnxr  10679  xltnegi  10695  xmullem  10736  xlemul1a  10760  xrsupsslem  10778  xrinfmsslem  10779  xrub  10783  xrsup0  10795  xrinfm0  10808  ixxdisj  10824  icodisj  10914  facdiv  11465  hasheqf1oi  11522  climuni  12233  rlimno1  12334  sqr2irr  12735  prmdvdsexpr  13003  prmfac1  13005  ramlb  13274  ram0  13277  prmlem1  13317  prmlem2  13329  pospo  14317  symgbas  14982  efgredlemc  15264  efgred  15267  psrvscafval  16345  prmirred  16665  0top  16938  pnfnei  17167  mnfnei  17168  cmpfi  17352  1stccnp  17405  filcon  17791  nmoleub2lem3  18811  ivthlem2  19027  ivthlem3  19028  ovolicc2lem3  19093  itg1addlem4  19269  itg2seq  19312  dvcnvlem  19538  lhop2  19577  bpos1  20745  lgsdir2lem2  20786  lgsqrlem2  20804  lgseisenlem2  20812  pntlem3  20981  ostth3  21010  uvtxisvtx  21169  uvtx01vtx  21171  ifeqeqx  23520  erdszelem4  24449  erdszelem8  24453  axlowdimlem15  25411  ordcmp  25713  finminlem  25823  nn0prpwlem  25830  nn0prpw  25831  smprngopr  26268  prtlem14  26333  jm2.23  26680  sdrgacs  27100  rzalf  27279  1to2vfriswmgra  27830  n4cyclfrgra  27842  frgrawopreg  27872  ax12-2  29162  a12stdy4  29188  lkrpssN  29412  atltcvr  29683  cdleme27a  30615  dihord6apre  31505  dihord6b  31509
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator