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  2974  eq0rdv  3464  rzal  3530  reusv2lem2  4508  dfwe2  4545  tfindsg  4623  findsg  4655  poirr2  5055  sofld  5109  omopth2  6550  swoord2  6658  unxpdomlem3  7037  suc11reg  7288  wemapwe  7368  r111  7415  r1pwss  7424  cflim2  7857  axunndlem1  8185  axunnd  8186  axpowndlem3  8189  axpownd  8191  axregndlem1  8192  axregndlem2  8193  axinfndlem1  8195  axinfnd  8196  axacndlem1  8197  axacndlem2  8198  axacndlem3  8199  axacndlem4  8200  axacndlem5  8201  axacnd  8202  fpwwe2lem13  8232  gchpwdom  8264  winalim2  8286  ltapr  8637  prodgt0  9569  squeeze0  9627  nnsub  9752  nn0sub  9982  elnnz  10002  indstr2  10264  uzsupss  10278  xrltnsym  10439  xrlttr  10442  qbtwnxr  10494  xltnegi  10510  xmullem  10551  xlemul1a  10575  xrsupsslem  10592  xrinfmsslem  10593  xrub  10597  xrsup0  10609  xrinfm0  10622  ixxdisj  10638  icodisj  10728  facdiv  11267  climuni  11992  rlimno1  12093  sqr2irr  12490  prmdvdsexpr  12758  prmfac1  12760  ramlb  13029  ram0  13032  prmlem1  13072  prmlem2  13084  pospo  14070  symgbas  14735  efgredlemc  15017  efgred  15020  psrvscafval  16098  prmirred  16411  0top  16684  pnfnei  16913  mnfnei  16914  cmpfi  17098  1stccnp  17151  filcon  17541  nmoleub2lem3  18559  ivthlem2  18775  ivthlem3  18776  ovolicc2lem3  18841  itg1addlem4  19017  itg2seq  19060  dvcnvlem  19286  lhop2  19325  bpos1  20485  lgsdir2lem2  20526  lgsqrlem2  20544  lgseisenlem2  20552  pntlem3  20721  ostth3  20750  ifeqeqx  22995  erdszelem4  23098  erdszelem8  23102  axlowdimlem15  23960  ordcmp  24262  nbssntrs  25515  finminlem  25599  nn0prpwlem  25606  nn0prpw  25607  smprngopr  26045  prtlem14  26110  jm2.23  26457  sdrgacs  26877  rzalf  27057  ax12-2  28353  a12stdy4  28379  lkrpssN  28603  atltcvr  28874  cdleme27a  29806  dihord6apre  30696  dihord6b  30700
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator