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

Theorem pm2.21d 101
Description: A contradiction implies anything. Deduction from pm2.21 103. (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 100 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21dd  102  pm2.21  103  2falsed  342  pm5.14  858  ecase2d  908  prlem1  930  sbc2or  3171  eq0rdv  3664  rzal  3731  reusv2lem2  4728  dfwe2  4765  tfindsg  4843  findsg  4875  poirr2  5261  sofld  5321  omopth2  6830  swoord2  6938  unxpdomlem3  7318  suc11reg  7577  wemapwe  7657  r111  7704  r1pwss  7713  cflim2  8148  axunndlem1  8475  axunnd  8476  axpowndlem3  8479  axpownd  8481  axregndlem1  8482  axregndlem2  8483  axinfndlem1  8485  axinfnd  8486  axacndlem1  8487  axacndlem2  8488  axacndlem3  8489  axacndlem4  8490  axacndlem5  8491  axacnd  8492  fpwwe2lem13  8522  gchpwdom  8550  winalim2  8576  ltapr  8927  prodgt0  9860  squeeze0  9918  nnsub  10043  nn0sub  10275  elnnz  10297  indstr2  10559  uzsupss  10573  xrltnsym  10735  xrlttr  10738  qbtwnxr  10791  xltnegi  10807  xmullem  10848  xlemul1a  10872  xrsupsslem  10890  xrinfmsslem  10891  xrub  10895  xrsup0  10907  xrinfm0  10920  ixxdisj  10936  icodisj  11027  facdiv  11583  hasheqf1oi  11640  climuni  12351  rlimno1  12452  sqr2irr  12853  prmdvdsexpr  13121  prmfac1  13123  ramlb  13392  ram0  13395  prmlem1  13435  prmlem2  13447  pospo  14435  symgbas  15100  efgredlemc  15382  efgred  15385  psrvscafval  16459  prmirred  16780  0top  17053  pnfnei  17289  mnfnei  17290  cmpfi  17476  1stccnp  17530  filcon  17920  ivthlem2  19354  ivthlem3  19355  ovolicc2lem3  19420  itg1addlem4  19594  itg2seq  19637  dvcnvlem  19865  lhop2  19904  bpos1  21072  lgsdir2lem2  21113  lgsqrlem2  21131  lgseisenlem2  21139  pntlem3  21308  ostth3  21337  uvtxisvtx  21504  uvtx01vtx  21506  ifeqeqx  24006  erdszelem4  24885  erdszelem8  24889  axlowdimlem15  25900  ordcmp  26202  finminlem  26335  nn0prpwlem  26339  nn0prpw  26340  smprngopr  26676  prtlem14  26737  jm2.23  27081  sdrgacs  27500  rzalf  27678  1to2vfriswmgra  28470  n4cyclfrgra  28482  frgranbnb  28484  frgrawopreg  28512  atltcvr  30306  dihord6apre  32128  dihord6b  32132
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator