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  3012  eq0rdv  3502  rzal  3568  reusv2lem2  4552  dfwe2  4589  tfindsg  4667  findsg  4699  poirr2  5083  sofld  5137  omopth2  6598  swoord2  6706  unxpdomlem3  7085  suc11reg  7336  wemapwe  7416  r111  7463  r1pwss  7472  cflim2  7905  axunndlem1  8233  axunnd  8234  axpowndlem3  8237  axpownd  8239  axregndlem1  8240  axregndlem2  8241  axinfndlem1  8243  axinfnd  8244  axacndlem1  8245  axacndlem2  8246  axacndlem3  8247  axacndlem4  8248  axacndlem5  8249  axacnd  8250  fpwwe2lem13  8280  gchpwdom  8312  winalim2  8334  ltapr  8685  prodgt0  9617  squeeze0  9675  nnsub  9800  nn0sub  10030  elnnz  10050  indstr2  10312  uzsupss  10326  xrltnsym  10487  xrlttr  10490  qbtwnxr  10543  xltnegi  10559  xmullem  10600  xlemul1a  10624  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  xrsup0  10658  xrinfm0  10671  ixxdisj  10687  icodisj  10777  facdiv  11316  climuni  12042  rlimno1  12143  sqr2irr  12543  prmdvdsexpr  12811  prmfac1  12813  ramlb  13082  ram0  13085  prmlem1  13125  prmlem2  13137  pospo  14123  symgbas  14788  efgredlemc  15070  efgred  15073  psrvscafval  16151  prmirred  16464  0top  16737  pnfnei  16966  mnfnei  16967  cmpfi  17151  1stccnp  17204  filcon  17594  nmoleub2lem3  18612  ivthlem2  18828  ivthlem3  18829  ovolicc2lem3  18894  itg1addlem4  19070  itg2seq  19113  dvcnvlem  19339  lhop2  19378  bpos1  20538  lgsdir2lem2  20579  lgsqrlem2  20597  lgseisenlem2  20605  pntlem3  20774  ostth3  20803  ifeqeqx  23050  erdszelem4  23740  erdszelem8  23744  axlowdimlem15  24656  ordcmp  24958  nbssntrs  26250  finminlem  26334  nn0prpwlem  26341  nn0prpw  26342  smprngopr  26780  prtlem14  26845  jm2.23  27192  sdrgacs  27612  rzalf  27791  uvtxisvtx  28303  uvtx01vtx  28305  1to2vfriswmgra  28430  n4cyclfrgra  28440  ax12-2  29725  a12stdy4  29751  lkrpssN  29975  atltcvr  30246  cdleme27a  31178  dihord6apre  32068  dihord6b  32072
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator