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

Theorem pm2.21d 100
Description: A contradiction implies anything. Deduction from pm2.21 102. (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 23 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 99 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21dd  101  pm2.21  102  2falsed  341  pm5.14  857  ecase2d  907  prlem1  929  sbc2or  3129  eq0rdv  3622  rzal  3689  reusv2lem2  4684  dfwe2  4721  tfindsg  4799  findsg  4831  poirr2  5217  sofld  5277  omopth2  6786  swoord2  6894  unxpdomlem3  7274  suc11reg  7530  wemapwe  7610  r111  7657  r1pwss  7666  cflim2  8099  axunndlem1  8426  axunnd  8427  axpowndlem3  8430  axpownd  8432  axregndlem1  8433  axregndlem2  8434  axinfndlem1  8436  axinfnd  8437  axacndlem1  8438  axacndlem2  8439  axacndlem3  8440  axacndlem4  8441  axacndlem5  8442  axacnd  8443  fpwwe2lem13  8473  gchpwdom  8505  winalim2  8527  ltapr  8878  prodgt0  9811  squeeze0  9869  nnsub  9994  nn0sub  10226  elnnz  10248  indstr2  10510  uzsupss  10524  xrltnsym  10686  xrlttr  10689  qbtwnxr  10742  xltnegi  10758  xmullem  10799  xlemul1a  10823  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  xrsup0  10858  xrinfm0  10871  ixxdisj  10887  icodisj  10978  facdiv  11533  hasheqf1oi  11590  climuni  12301  rlimno1  12402  sqr2irr  12803  prmdvdsexpr  13071  prmfac1  13073  ramlb  13342  ram0  13345  prmlem1  13385  prmlem2  13397  pospo  14385  symgbas  15050  efgredlemc  15332  efgred  15335  psrvscafval  16409  prmirred  16730  0top  17003  pnfnei  17238  mnfnei  17239  cmpfi  17425  1stccnp  17478  filcon  17868  ivthlem2  19302  ivthlem3  19303  ovolicc2lem3  19368  itg1addlem4  19544  itg2seq  19587  dvcnvlem  19813  lhop2  19852  bpos1  21020  lgsdir2lem2  21061  lgsqrlem2  21079  lgseisenlem2  21087  pntlem3  21256  ostth3  21285  uvtxisvtx  21452  uvtx01vtx  21454  ifeqeqx  23954  erdszelem4  24833  erdszelem8  24837  axlowdimlem15  25799  ordcmp  26101  finminlem  26211  nn0prpwlem  26215  nn0prpw  26216  smprngopr  26552  prtlem14  26613  jm2.23  26957  sdrgacs  27377  rzalf  27555  swrdccat3b  28031  1to2vfriswmgra  28110  n4cyclfrgra  28122  frgranbnb  28124  frgrawopreg  28152  atltcvr  29917  dihord6apre  31739  dihord6b  31743
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator