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  3133  eq0rdv  3626  rzal  3693  reusv2lem2  4688  dfwe2  4725  tfindsg  4803  findsg  4835  poirr2  5221  sofld  5281  omopth2  6790  swoord2  6898  unxpdomlem3  7278  suc11reg  7534  wemapwe  7614  r111  7661  r1pwss  7670  cflim2  8103  axunndlem1  8430  axunnd  8431  axpowndlem3  8434  axpownd  8436  axregndlem1  8437  axregndlem2  8438  axinfndlem1  8440  axinfnd  8441  axacndlem1  8442  axacndlem2  8443  axacndlem3  8444  axacndlem4  8445  axacndlem5  8446  axacnd  8447  fpwwe2lem13  8477  gchpwdom  8509  winalim2  8531  ltapr  8882  prodgt0  9815  squeeze0  9873  nnsub  9998  nn0sub  10230  elnnz  10252  indstr2  10514  uzsupss  10528  xrltnsym  10690  xrlttr  10693  qbtwnxr  10746  xltnegi  10762  xmullem  10803  xlemul1a  10827  xrsupsslem  10845  xrinfmsslem  10846  xrub  10850  xrsup0  10862  xrinfm0  10875  ixxdisj  10891  icodisj  10982  facdiv  11537  hasheqf1oi  11594  climuni  12305  rlimno1  12406  sqr2irr  12807  prmdvdsexpr  13075  prmfac1  13077  ramlb  13346  ram0  13349  prmlem1  13389  prmlem2  13401  pospo  14389  symgbas  15054  efgredlemc  15336  efgred  15339  psrvscafval  16413  prmirred  16734  0top  17007  pnfnei  17242  mnfnei  17243  cmpfi  17429  1stccnp  17482  filcon  17872  ivthlem2  19306  ivthlem3  19307  ovolicc2lem3  19372  itg1addlem4  19548  itg2seq  19591  dvcnvlem  19817  lhop2  19856  bpos1  21024  lgsdir2lem2  21065  lgsqrlem2  21083  lgseisenlem2  21091  pntlem3  21260  ostth3  21289  uvtxisvtx  21456  uvtx01vtx  21458  ifeqeqx  23958  erdszelem4  24837  erdszelem8  24841  axlowdimlem15  25803  ordcmp  26105  finminlem  26215  nn0prpwlem  26219  nn0prpw  26220  smprngopr  26556  prtlem14  26617  jm2.23  26961  sdrgacs  27381  rzalf  27559  swrdccat3b  28035  1to2vfriswmgra  28114  n4cyclfrgra  28126  frgranbnb  28128  frgrawopreg  28156  atltcvr  29921  dihord6apre  31743  dihord6b  31747
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator