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 4668 vs. uniexg 4669. (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  2018  equviniOLD  2044  equveliOLD  2046  ax11v  2149  sbal1  2180  dvelimALT  2187  ax11  2209  hbequid  2214  dvelimf-o  2234  ax11eq  2247  ax11el  2248  ax11indalem  2251  ax11inda2ALT  2252  ax11inda2  2253  euan  2315  moexex  2327  rgen2a  2736  ralrimivw  2754  reximdv  2781  rexlimdvw  2797  reuind  3101  rexn0  3694  tppreqb  3903  prnebg  3943  axsep  4293  dtru  4354  fr0  4525  ordsssuc2  4633  reusv6OLD  4697  reusv7OLD  4698  ordsucelsuc  4765  tfinds  4802  tfindsg  4803  limomss  4813  findsg  4835  finds1  4837  ssrel2  4929  poltletr  5232  xpexr  5270  ndmfv  5718  fveqres  5727  fmptco  5864  elunirnALT  5963  ndmovord  6200  bropopvvv  6389  soxp  6422  mpt2xopynvov0  6432  smofvon2  6581  abianfplem  6678  oaordi  6752  oawordeulem  6760  odi  6785  brdomg  7081  map1  7148  fopwdom  7179  fodomr  7221  mapxpen  7236  infensuc  7248  onomeneq  7259  fineqvlem  7286  fineqv  7287  pssnn  7290  xpfi  7341  finsschain  7375  dffi3  7398  fisup2g  7431  fisupcl  7432  inf3lemd  7542  en3lplem2  7631  r1ordg  7664  r1val1  7672  r1pw  7731  r1pwOLD  7732  rankxplim3  7765  carddomi2  7817  fidomtri  7840  pr2ne  7849  alephon  7910  alephcard  7911  alephnbtwn  7912  alephordi  7915  iunfictbso  7955  fin23lem30  8182  fin1a2lem10  8249  domtriomlem  8282  axdc3lem2  8291  axdc3lem4  8293  alephval2  8407  cfpwsdom  8419  axextnd  8426  axrepnd  8429  axpownd  8436  axregnd  8439  axinfndlem1  8440  fpwwe2lem12  8476  wunfi  8556  addnidpi  8738  pinq  8764  ltexprlem7  8879  mulgt0sr  8940  nnind  9978  nn1m1nn  9980  nn0n0n1ge2b  10241  uzindOLD  10324  uzm1  10476  xrltnsym  10690  xrlttri  10692  xrlttr  10693  qbtwnxr  10746  xltnegi  10762  xlt2add  10799  xrsupsslem  10845  xrinfmsslem  10846  xrub  10850  fzospliti  11124  elfznelfzo  11151  injresinjlem  11158  injresinj  11159  seqfveq2  11304  seqshft2  11308  monoord  11312  seqsplit  11315  seqf1o  11323  seqhomo  11329  faclbnd4lem4  11546  hasheqf1oi  11594  hashgt0elex  11629  hash1snb  11640  hashf1lem2  11664  hashf1  11665  seqcoll  11671  resqrex  12015  rexuz3  12111  rexanuz2  12112  limsupgre  12234  rlimconst  12297  caurcvg  12429  caucvg  12431  sumss  12477  fsumcl2lem  12484  fsumrlim  12549  fsumo1  12550  nn0seqcvgd  13020  exprmfct  13069  rpexp1i  13080  pcz  13213  pcadd  13217  pcmptcl  13219  prmlem0  13387  ressress  13485  sylow1lem1  15191  efgsf  15320  efgrelexlema  15340  dprdss  15546  ablfac1eulem  15589  lssssr  15988  psrvscafval  16413  mplcoe1  16487  mplcoe2  16489  epttop  17032  neiptopnei  17155  cmpsublem  17420  fiuncmp  17425  1stcrest  17473  kgenss  17532  hmeofval  17747  fbun  17829  fgss2  17863  filcon  17872  filuni  17874  filssufilg  17900  filufint  17909  hausflimi  17969  hausflim  17970  hauspwpwf1  17976  fclscmp  18019  alexsubALTlem4  18038  ptcmplem3  18042  ptcmplem5  18044  cstucnd  18271  isxmet2d  18314  imasdsf1olem  18360  blfps  18393  blf  18394  metrest  18511  nrginvrcn  18684  nmoge0  18712  nmoleub  18722  fsumcn  18857  cmetcaulem  19198  iscmet3  19203  iscmet2  19204  bcthlem2  19235  ovolicc2lem3  19372  itg2seq  19591  itg2splitlem  19597  itgeq1f  19620  itgeq2  19626  iblcnlem  19637  itgfsum  19675  limcnlp  19722  perfdvf  19747  dvnres  19774  dvmptfsum  19816  c1lip1  19838  mpfrcl  19896  aalioulem5  20210  abelth  20314  sinq12ge0  20373  rlimcnp  20761  xrlimcnp  20764  jensen  20784  ppiublem1  20943  dchrelbas3  20979  bcmono  21018  lgsquad2lem2  21100  2sqlem10  21115  pntrsumbnd2  21218  pntpbnd1  21237  pntlem3  21260  ausisusgra  21337  usgraidx2v  21369  nbgra0nb  21398  nbgranself2  21405  nbgraf1olem3  21410  nbgraf1olem5  21412  nb3graprlem1  21417  nbcusgra  21429  cusgrasizeinds  21442  uvtxnbgra  21459  wlkdvspthlem  21564  fargshiftfo  21582  3v3e3cycl1  21588  4cycl4v4e  21610  4cycl4dv4e  21612  vdgrf  21626  eupai  21646  eupath2  21659  isexid2  21870  zerdivemp1  21979  shsvs  22782  0cnop  23439  0cnfn  23440  cnlnssadj  23540  ssmd1  23771  ssmd2  23772  atexch  23841  mdsymlem4  23866  sumdmdlem  23878  ifeqeqx  23958  fmptcof2  24033  pwsiga  24470  subfacp1lem6  24828  erdszelem8  24841  cvmliftlem7  24935  cvmliftlem10  24938  cvmlift2lem12  24958  dedekind  25144  fprodcl2lem  25233  trpredlem1  25448  poseq  25471  funpartfv  25702  axlowdimlem15  25803  axcontlem7  25817  endofsegid  25927  broutsideof2  25964  ordcmp  26105  findreccl  26111  ovoliunnfl  26151  voliunnfl  26153  volsupnfl  26154  itg2addnclem3  26161  itg2addnc  26162  areacirclem2  26185  a1i13  26192  a1i24  26195  nn0prpwlem  26219  nn0prpw  26220  sdclem2  26340  fdc  26343  mettrifi  26357  zerdivemp1x  26465  smprngopr  26556  jca3  26587  monotoddzzfi  26899  psgnunilem4  27292  refsum2cnlem1  27579  stoweidlem31  27651  reuan  27829  2reu4  27839  funressnfv  27863  ndmaovass  27941  otsndisj  27957  otiunsndisj  27958  otiunsndisjX  27959  euhash1  28002  swrdnd  28005  swrdswrd  28015  swrdccatin1  28020  swrdccatin2  28022  swrdccatin12lem3a  28025  swrdccatin12lem4  28029  swrdccat3  28033  usgra2pthspth  28039  usgra2wlkspthlem1  28040  usgra2pth  28045  el2wlkonotot0  28073  usg2wlkonot  28084  usg2wotspth  28085  2spontn0vne  28088  frgra2v  28107  frgra3vlem1  28108  3vfriswmgralem  28112  1to2vfriswmgra  28114  1to3vfriswmgra  28115  2pthfrgra  28119  frgranbnb  28128  vdfrgra0  28130  vdgfrgra0  28131  vdn1frgrav2  28134  vdgn1frgrav2  28135  vdgfrgragt2  28136  frgrawopreglem2  28152  frgrawopreglem3  28153  frgrawopreglem4  28154  frgrawopreg  28156  frgraregorufr0  28159  frgraregorufr  28160  2spotdisj  28168  2spotiundisj  28169  2spotmdisj  28175  ad4ant14  28257  ad4ant134  28260  ee121  28302  ee122  28303  rspsbc2  28333  a9e2ndeq  28361  vd12  28414  vd13  28415  ee221  28464  ee212  28466  ee112  28469  ee211  28472  ee210  28474  ee201  28476  ee120  28478  ee021  28480  ee012  28482  ee102  28484  ee03  28566  ee31  28577  ee31an  28579  ee123  28588  a9e2ndeqVD  28734  a9e2ndeqALT  28757  bnj151  28958  bnj594  28993  bnj600  29000  dvelimvNEW7  29172  equsalNEW7  29197  dvelimhvAUX7  29202  equviniNEW7  29235  equveliNEW7  29236  ax11vNEW7  29300  sbal1NEW7  29320  dvelimALTNEW7  29341  dvelimhOLD7  29401  lfl1dim  29608  lfl1dim2N  29609  lkreqN  29657  cvrexchlem  29905  ps-2  29964  paddasslem14  30319  idldil  30600  isltrn2N  30606  cdleme25a  30839  dibglbN  31653  dihlsscpre  31721  dvh4dimlem  31930  lcfl7N  31988  mapdval2N  32117
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator