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  2999  eq0rdv  3489  rzal  3555  reusv2lem2  4536  dfwe2  4573  tfindsg  4651  findsg  4683  poirr2  5067  sofld  5121  omopth2  6582  swoord2  6690  unxpdomlem3  7069  suc11reg  7320  wemapwe  7400  r111  7447  r1pwss  7456  cflim2  7889  axunndlem1  8217  axunnd  8218  axpowndlem3  8221  axpownd  8223  axregndlem1  8224  axregndlem2  8225  axinfndlem1  8227  axinfnd  8228  axacndlem1  8229  axacndlem2  8230  axacndlem3  8231  axacndlem4  8232  axacndlem5  8233  axacnd  8234  fpwwe2lem13  8264  gchpwdom  8296  winalim2  8318  ltapr  8669  prodgt0  9601  squeeze0  9659  nnsub  9784  nn0sub  10014  elnnz  10034  indstr2  10296  uzsupss  10310  xrltnsym  10471  xrlttr  10474  qbtwnxr  10527  xltnegi  10543  xmullem  10584  xlemul1a  10608  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  xrsup0  10642  xrinfm0  10655  ixxdisj  10671  icodisj  10761  facdiv  11300  climuni  12026  rlimno1  12127  sqr2irr  12527  prmdvdsexpr  12795  prmfac1  12797  ramlb  13066  ram0  13069  prmlem1  13109  prmlem2  13121  pospo  14107  symgbas  14772  efgredlemc  15054  efgred  15057  psrvscafval  16135  prmirred  16448  0top  16721  pnfnei  16950  mnfnei  16951  cmpfi  17135  1stccnp  17188  filcon  17578  nmoleub2lem3  18596  ivthlem2  18812  ivthlem3  18813  ovolicc2lem3  18878  itg1addlem4  19054  itg2seq  19097  dvcnvlem  19323  lhop2  19362  bpos1  20522  lgsdir2lem2  20563  lgsqrlem2  20581  lgseisenlem2  20589  pntlem3  20758  ostth3  20787  ifeqeqx  23034  erdszelem4  23725  erdszelem8  23729  axlowdimlem15  24584  ordcmp  24886  nbssntrs  26147  finminlem  26231  nn0prpwlem  26238  nn0prpw  26239  smprngopr  26677  prtlem14  26742  jm2.23  27089  sdrgacs  27509  rzalf  27688  uvtxisvtx  28162  uvtx01vtx  28164  1to2vfriswmgra  28184  ax12-2  29103  a12stdy4  29129  lkrpssN  29353  atltcvr  29624  cdleme27a  30556  dihord6apre  31446  dihord6b  31450
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator