MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1d Unicode version

Theorem a1d 23
Description: Deduction introducing an embedded antecedent.

Naming convention: We often call a theorem a "deduction" and suffix its label with "d" whenever the hypotheses and conclusion are each prefixed with the same antecedent. This allows us to use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used; here  ph would be replaced with a conjunction (df-an 361) of the hypotheses of the would-be deduction. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 11. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 5. We usually show the theorem form without a suffix on its label (e.g. pm2.43 49 vs. pm2.43i 45 vs. pm2.43d 46). When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for "more general") as in uniex 4664 vs. uniexg 4665. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

Hypothesis
Ref Expression
a1d.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
a1d  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem a1d
StepHypRef Expression
1 a1d.1 . 2  |-  ( ph  ->  ps )
2 ax-1 5 . 2  |-  ( ps 
->  ( ch  ->  ps ) )
31, 2syl 16 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  a1iiALT  26  syl5com  28  mpid  39  syld  42  imim2d  50  syl5d  64  syl6d  66  pm2.21d  100  pm2.24d  137  pm2.51  147  pm2.521  148  pm2.61iii  161  mtod  170  impbid21d  183  imbi2d  308  adantr  452  jctild  528  jctird  529  pm3.4  545  anbi2d  685  anbi1d  686  3ecase  1288  ee21  1381  meredith  1410  equsalhwOLD  1857  equsalOLD  1967  dvelimvOLD  1994  dvelimhOLD  2016  equviniOLD  2041  equveliOLD  2043  ax11v  2145  sbal1  2176  dvelimALT  2183  ax11  2205  hbequid  2210  dvelimf-o  2230  ax11eq  2243  ax11el  2244  ax11indalem  2247  ax11inda2ALT  2248  ax11inda2  2249  euan  2311  moexex  2323  rgen2a  2732  ralrimivw  2750  reximdv  2777  rexlimdvw  2793  reuind  3097  rexn0  3690  tppreqb  3899  prnebg  3939  axsep  4289  dtru  4350  fr0  4521  ordsssuc2  4629  reusv6OLD  4693  reusv7OLD  4694  ordsucelsuc  4761  tfinds  4798  tfindsg  4799  limomss  4809  findsg  4831  finds1  4833  ssrel2  4925  poltletr  5228  xpexr  5266  ndmfv  5714  fveqres  5723  fmptco  5860  elunirnALT  5959  ndmovord  6196  bropopvvv  6385  soxp  6418  mpt2xopynvov0  6428  smofvon2  6577  abianfplem  6674  oaordi  6748  oawordeulem  6756  odi  6781  brdomg  7077  map1  7144  fopwdom  7175  fodomr  7217  mapxpen  7232  infensuc  7244  onomeneq  7255  fineqvlem  7282  fineqv  7283  pssnn  7286  xpfi  7337  finsschain  7371  dffi3  7394  fisup2g  7427  fisupcl  7428  inf3lemd  7538  en3lplem2  7627  r1ordg  7660  r1val1  7668  r1pw  7727  r1pwOLD  7728  rankxplim3  7761  carddomi2  7813  fidomtri  7836  pr2ne  7845  alephon  7906  alephcard  7907  alephnbtwn  7908  alephordi  7911  iunfictbso  7951  fin23lem30  8178  fin1a2lem10  8245  domtriomlem  8278  axdc3lem2  8287  axdc3lem4  8289  alephval2  8403  cfpwsdom  8415  axextnd  8422  axrepnd  8425  axpownd  8432  axregnd  8435  axinfndlem1  8436  fpwwe2lem12  8472  wunfi  8552  addnidpi  8734  pinq  8760  ltexprlem7  8875  mulgt0sr  8936  nnind  9974  nn1m1nn  9976  nn0n0n1ge2b  10237  uzindOLD  10320  uzm1  10472  xrltnsym  10686  xrlttri  10688  xrlttr  10689  qbtwnxr  10742  xltnegi  10758  xlt2add  10795  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  fzospliti  11120  elfznelfzo  11147  injresinjlem  11154  injresinj  11155  seqfveq2  11300  seqshft2  11304  monoord  11308  seqsplit  11311  seqf1o  11319  seqhomo  11325  faclbnd4lem4  11542  hasheqf1oi  11590  hashgt0elex  11625  hash1snb  11636  hashf1lem2  11660  hashf1  11661  seqcoll  11667  resqrex  12011  rexuz3  12107  rexanuz2  12108  limsupgre  12230  rlimconst  12293  caurcvg  12425  caucvg  12427  sumss  12473  fsumcl2lem  12480  fsumrlim  12545  fsumo1  12546  nn0seqcvgd  13016  exprmfct  13065  rpexp1i  13076  pcz  13209  pcadd  13213  pcmptcl  13215  prmlem0  13383  ressress  13481  sylow1lem1  15187  efgsf  15316  efgrelexlema  15336  dprdss  15542  ablfac1eulem  15585  lssssr  15984  psrvscafval  16409  mplcoe1  16483  mplcoe2  16485  epttop  17028  neiptopnei  17151  cmpsublem  17416  fiuncmp  17421  1stcrest  17469  kgenss  17528  hmeofval  17743  fbun  17825  fgss2  17859  filcon  17868  filuni  17870  filssufilg  17896  filufint  17905  hausflimi  17965  hausflim  17966  hauspwpwf1  17972  fclscmp  18015  alexsubALTlem4  18034  ptcmplem3  18038  ptcmplem5  18040  cstucnd  18267  isxmet2d  18310  imasdsf1olem  18356  blfps  18389  blf  18390  metrest  18507  nrginvrcn  18680  nmoge0  18708  nmoleub  18718  fsumcn  18853  cmetcaulem  19194  iscmet3  19199  iscmet2  19200  bcthlem2  19231  ovolicc2lem3  19368  itg2seq  19587  itg2splitlem  19593  itgeq1f  19616  itgeq2  19622  iblcnlem  19633  itgfsum  19671  limcnlp  19718  perfdvf  19743  dvnres  19770  dvmptfsum  19812  c1lip1  19834  mpfrcl  19892  aalioulem5  20206  abelth  20310  sinq12ge0  20369  rlimcnp  20757  xrlimcnp  20760  jensen  20780  ppiublem1  20939  dchrelbas3  20975  bcmono  21014  lgsquad2lem2  21096  2sqlem10  21111  pntrsumbnd2  21214  pntpbnd1  21233  pntlem3  21256  ausisusgra  21333  usgraidx2v  21365  nbgra0nb  21394  nbgranself2  21401  nbgraf1olem3  21406  nbgraf1olem5  21408  nb3graprlem1  21413  nbcusgra  21425  cusgrasizeinds  21438  uvtxnbgra  21455  wlkdvspthlem  21560  fargshiftfo  21578  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  vdgrf  21622  eupai  21642  eupath2  21655  isexid2  21866  zerdivemp1  21975  shsvs  22778  0cnop  23435  0cnfn  23436  cnlnssadj  23536  ssmd1  23767  ssmd2  23768  atexch  23837  mdsymlem4  23862  sumdmdlem  23874  ifeqeqx  23954  fmptcof2  24029  pwsiga  24466  subfacp1lem6  24824  erdszelem8  24837  cvmliftlem7  24931  cvmliftlem10  24934  cvmlift2lem12  24954  dedekind  25140  fprodcl2lem  25229  trpredlem1  25444  poseq  25467  funpartfv  25698  axlowdimlem15  25799  axcontlem7  25813  endofsegid  25923  broutsideof2  25960  ordcmp  26101  findreccl  26107  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  itg2addnclem3  26157  itg2addnc  26158  areacirclem2  26181  a1i13  26188  a1i24  26191  nn0prpwlem  26215  nn0prpw  26216  sdclem2  26336  fdc  26339  mettrifi  26353  zerdivemp1x  26461  smprngopr  26552  jca3  26583  monotoddzzfi  26895  psgnunilem4  27288  refsum2cnlem1  27575  stoweidlem31  27647  reuan  27825  2reu4  27835  funressnfv  27859  ndmaovass  27937  otsndisj  27953  otiunsndisj  27954  otiunsndisjX  27955  euhash1  27998  swrdnd  28001  swrdswrd  28011  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12lem3a  28021  swrdccatin12lem4  28025  swrdccat3  28029  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2pth  28041  el2wlkonotot0  28069  usg2wlkonot  28080  usg2wotspth  28081  2spontn0vne  28084  frgra2v  28103  frgra3vlem1  28104  3vfriswmgralem  28108  1to2vfriswmgra  28110  1to3vfriswmgra  28111  2pthfrgra  28115  frgranbnb  28124  vdfrgra0  28126  vdgfrgra0  28127  vdn1frgrav2  28130  vdgn1frgrav2  28131  vdgfrgragt2  28132  frgrawopreglem2  28148  frgrawopreglem3  28149  frgrawopreglem4  28150  frgrawopreg  28152  frgraregorufr0  28155  frgraregorufr  28156  2spotdisj  28164  2spotiundisj  28165  2spotmdisj  28171  ad4ant14  28253  ad4ant134  28256  ee121  28298  ee122  28299  rspsbc2  28329  a9e2ndeq  28357  vd12  28410  vd13  28411  ee221  28460  ee212  28462  ee112  28465  ee211  28468  ee210  28470  ee201  28472  ee120  28474  ee021  28476  ee012  28478  ee102  28480  ee03  28562  ee31  28573  ee31an  28575  ee123  28584  a9e2ndeqVD  28730  a9e2ndeqALT  28753  bnj151  28954  bnj594  28989  bnj600  28996  dvelimvNEW7  29168  equsalNEW7  29193  dvelimhvAUX7  29198  equviniNEW7  29231  equveliNEW7  29232  ax11vNEW7  29296  sbal1NEW7  29316  dvelimALTNEW7  29337  dvelimhOLD7  29397  lfl1dim  29604  lfl1dim2N  29605  lkreqN  29653  cvrexchlem  29901  ps-2  29960  paddasslem14  30315  idldil  30596  isltrn2N  30602  cdleme25a  30835  dibglbN  31649  dihlsscpre  31717  dvh4dimlem  31926  lcfl7N  31984  mapdval2N  32113
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator