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

Theorem pm2.21d 106
Description: A contradiction implies anything. Deduction from pm2.21 108. (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 25 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 105 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.21ddOLD  107  pm2.21  108  2falsed  351  pm5.14  881  ecase2d  931  prlem1  953  sbc2or  3200  sbcimdv  3260  eq0rdv  3677  csbprc  3678  rzal  3786  reusv2lem2  4499  poirr2  5227  sofld  5291  dfwe2  6398  tfindsg  6476  findsg  6508  omopth2  7028  swoord2  7136  unxpdomlem3  7524  suc11reg  7830  wemapwe  7933  wemapweOLD  7934  r111  7987  r1pwss  7996  cflim2  8437  axunndlem1  8764  axunnd  8765  axpowndlem3  8769  axpowndlem3OLD  8770  axpownd  8772  axregndlem1  8773  axregndlem2  8774  axinfndlem1  8777  axinfnd  8778  axacndlem1  8779  axacndlem2  8780  axacndlem3  8781  axacndlem4  8782  axacndlem5  8783  axacnd  8784  fpwwe2lem13  8814  gchpwdom  8842  winalim2  8868  ltapr  9219  prodgt0  10179  squeeze0  10240  nnsub  10365  nn0sub  10635  elnnz  10661  indstr2  10938  uzsupss  10952  xrltnsym  11119  xrlttr  11122  qbtwnxr  11175  xltnegi  11191  xmullem  11232  xlemul1a  11256  xrsupsslem  11274  xrinfmsslem  11275  xrub  11279  xrsup0  11291  xrinfm0  11304  ixxdisj  11320  icodisj  11415  facdiv  12068  hasheqf1oi  12127  swrd0  12332  climuni  13035  rlimno1  13136  sqr2irr  13536  prmdvdsexpr  13807  prmfac1  13809  ramlb  14085  ram0  14088  prmlem1  14140  prmlem2  14152  pospo  15148  symgbas  15890  efgredlemc  16247  efgred  16250  psrvscafval  17466  prmirred  17924  prmirredOLD  17927  0top  18593  pnfnei  18829  mnfnei  18830  cmpfi  19016  1stccnp  19071  filcon  19461  ivthlem2  20941  ivthlem3  20942  ovolicc2lem3  21007  itg1addlem4  21182  itg2seq  21225  dvcnvlem  21453  lhop2  21492  bpos1  22627  lgsdir2lem2  22668  lgsqrlem2  22686  lgseisenlem2  22694  pntlem3  22863  ostth3  22892  axlowdimlem15  23207  uvtxisvtx  23403  uvtx01vtx  23405  ifeqeqx  25907  erdszelem4  27087  erdszelem8  27091  ordcmp  28298  finminlem  28518  nn0prpwlem  28522  nn0prpw  28523  smprngopr  28857  prtlem14  29024  jm2.23  29350  sdrgacs  29563  rzalf  29744  nn01to3  30192  wlkv0  30296  1to2vfriswmgra  30603  n4cyclfrgra  30615  frgranbnb  30617  frgrawopreg  30647  frgraregord013  30716  ztprmneprm  30744  atltcvr  33084  dihord6apre  34906  dihord6b  34910
  Copyright terms: Public domain W3C validator