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  874  ecase2d  924  prlem1  946  sbc2or  3183  sbcimdv  3243  eq0rdv  3660  csbprc  3661  rzal  3769  reusv2lem2  4482  poirr2  5210  sofld  5274  dfwe2  6382  tfindsg  6460  findsg  6492  omopth2  7011  swoord2  7119  unxpdomlem3  7507  suc11reg  7813  wemapwe  7916  wemapweOLD  7917  r111  7970  r1pwss  7979  cflim2  8420  axunndlem1  8747  axunnd  8748  axpowndlem3  8752  axpowndlem3OLD  8753  axpownd  8755  axregndlem1  8756  axregndlem2  8757  axinfndlem1  8759  axinfnd  8760  axacndlem1  8761  axacndlem2  8762  axacndlem3  8763  axacndlem4  8764  axacndlem5  8765  axacnd  8766  fpwwe2lem13  8796  gchpwdom  8824  winalim2  8850  ltapr  9201  prodgt0  10161  squeeze0  10222  nnsub  10347  nn0sub  10617  elnnz  10643  indstr2  10920  uzsupss  10934  xrltnsym  11101  xrlttr  11104  qbtwnxr  11157  xltnegi  11173  xmullem  11214  xlemul1a  11238  xrsupsslem  11256  xrinfmsslem  11257  xrub  11261  xrsup0  11273  xrinfm0  11286  ixxdisj  11302  icodisj  11396  facdiv  12046  hasheqf1oi  12105  swrd0  12310  climuni  13013  rlimno1  13114  sqr2irr  13513  prmdvdsexpr  13784  prmfac1  13786  ramlb  14062  ram0  14065  prmlem1  14117  prmlem2  14129  pospo  15125  symgbas  15864  efgredlemc  16221  efgred  16224  psrvscafval  17394  prmirred  17760  prmirredOLD  17763  0top  18429  pnfnei  18665  mnfnei  18666  cmpfi  18852  1stccnp  18907  filcon  19297  ivthlem2  20777  ivthlem3  20778  ovolicc2lem3  20843  itg1addlem4  21018  itg2seq  21061  dvcnvlem  21289  lhop2  21328  bpos1  22506  lgsdir2lem2  22547  lgsqrlem2  22565  lgseisenlem2  22573  pntlem3  22742  ostth3  22771  axlowdimlem15  23024  uvtxisvtx  23220  uvtx01vtx  23222  ifeqeqx  25725  erdszelem4  26929  erdszelem8  26933  ordcmp  28140  finminlem  28354  nn0prpwlem  28358  nn0prpw  28359  smprngopr  28693  prtlem14  28861  jm2.23  29187  sdrgacs  29400  rzalf  29581  nn01to3  30030  wlkv0  30134  1to2vfriswmgra  30441  n4cyclfrgra  30453  frgranbnb  30455  frgrawopreg  30485  frgraregord013  30554  ztprmneprm  30580  atltcvr  32649  dihord6apre  34471  dihord6b  34475
  Copyright terms: Public domain W3C validator