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 24 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 99 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  pm2.21dd  101  pm2.21  102  2falsed  342  pm5.14  861  ecase2d  911  prlem1  933  sbc2or  2929  eq0rdv  3396  rzal  3461  reusv2lem2  4427  dfwe2  4464  tfindsg  4542  findsg  4574  poirr2  4974  sofld  5028  omopth2  6468  swoord2  6576  unxpdomlem3  6954  suc11reg  7204  wemapwe  7284  r111  7331  r1pwss  7340  cflim2  7773  axunndlem1  8097  axunnd  8098  axpowndlem3  8101  axpownd  8103  axregndlem1  8104  axregndlem2  8105  axinfndlem1  8107  axinfnd  8108  axacndlem1  8109  axacndlem2  8110  axacndlem3  8111  axacndlem4  8112  axacndlem5  8113  axacnd  8114  fpwwe2lem13  8144  gchpwdom  8176  winalim2  8198  ltapr  8549  prodgt0  9481  squeeze0  9539  nnsub  9664  nn0sub  9893  elnnz  9913  indstr2  10175  uzsupss  10189  xrltnsym  10350  xrlttr  10353  qbtwnxr  10405  xltnegi  10421  xmullem  10462  xlemul1a  10486  xrsupsslem  10503  xrinfmsslem  10504  xrub  10508  xrsup0  10520  xrinfm0  10533  ixxdisj  10549  icodisj  10639  facdiv  11178  climuni  11903  rlimno1  12004  sqr2irr  12401  prmdvdsexpr  12669  prmfac1  12671  ramlb  12940  ram0  12943  prmlem1  12983  prmlem2  12995  pospo  13951  symgbas  14607  efgredlemc  14889  efgred  14892  psrvscafval  15967  prmirred  16280  0top  16553  pnfnei  16782  mnfnei  16783  cmpfi  16967  1stccnp  17020  filcon  17410  nmoleub2lem3  18428  ivthlem2  18644  ivthlem3  18645  ovolicc2lem3  18710  itg1addlem4  18886  itg2seq  18929  dvcnvlem  19155  lhop2  19194  bpos1  20354  lgsdir2lem2  20395  lgsqrlem2  20413  lgseisenlem2  20421  pntlem3  20590  ostth3  20619  erdszelem4  22896  erdszelem8  22900  axlowdimlem15  23758  ordcmp  24060  nbssntrs  25313  finminlem  25397  nn0prpwlem  25404  nn0prpw  25405  smprngopr  25843  prtlem14  25908  jm2.23  26255  sdrgacs  26675  ax12-2  27792  a12stdy4  27818  lkrpssN  28042  atltcvr  28313  cdleme27a  29245  dihord6apre  30135  dihord6b  30139
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator