MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1d Structured version   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 4705 vs. uniexg 4706. (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  1384  meredith  1413  equsalhwOLD  1861  equsalOLD  2000  dvelimvOLD  2028  dvelimhOLD  2072  equviniOLD  2084  equveliOLD  2086  nfsb4t  2127  ax11v  2172  sbal1  2203  dvelimALT  2210  ax11  2232  hbequid  2237  dvelimf-o  2257  ax11eq  2270  ax11el  2271  ax11indalem  2274  ax11inda2ALT  2275  ax11inda2  2276  euan  2338  moexex  2350  rgen2a  2772  ralrimivw  2790  reximdv  2817  rexlimdvw  2833  reuind  3137  rexn0  3730  tppreqb  3939  prnebg  3979  axsep  4329  dtru  4390  fr0  4561  ordsssuc2  4670  reusv6OLD  4734  reusv7OLD  4735  ordsucelsuc  4802  tfinds  4839  tfindsg  4840  limomss  4850  findsg  4872  finds1  4874  ssrel2  4966  poltletr  5269  xpexr  5307  ndmfv  5755  fveqres  5764  fmptco  5901  elunirnALT  6000  ndmovord  6237  bropopvvv  6426  soxp  6459  mpt2xopynvov0  6469  smofvon2  6618  abianfplem  6715  oaordi  6789  oawordeulem  6797  odi  6822  brdomg  7118  map1  7185  fopwdom  7216  fodomr  7258  mapxpen  7273  infensuc  7285  onomeneq  7296  fineqvlem  7323  fineqv  7324  pssnn  7327  xpfi  7378  finsschain  7413  dffi3  7436  fisup2g  7471  fisupcl  7472  inf3lemd  7582  en3lplem2  7671  r1ordg  7704  r1val1  7712  r1pw  7771  r1pwOLD  7772  rankxplim3  7805  carddomi2  7857  fidomtri  7880  pr2ne  7889  alephon  7950  alephcard  7951  alephnbtwn  7952  alephordi  7955  iunfictbso  7995  fin23lem30  8222  fin1a2lem10  8289  domtriomlem  8322  axdc3lem2  8331  axdc3lem4  8333  alephval2  8447  cfpwsdom  8459  axextnd  8466  axrepnd  8469  axpownd  8476  axregnd  8479  axinfndlem1  8480  fpwwe2lem12  8516  wunfi  8596  addnidpi  8778  pinq  8804  ltexprlem7  8919  mulgt0sr  8980  nnind  10018  nn1m1nn  10020  nn0n0n1ge2b  10281  uzindOLD  10364  uzm1  10516  xrltnsym  10730  xrlttri  10732  xrlttr  10733  qbtwnxr  10786  xltnegi  10802  xlt2add  10839  xrsupsslem  10885  xrinfmsslem  10886  xrub  10890  fzospliti  11165  elfznelfzo  11192  injresinjlem  11199  injresinj  11200  seqfveq2  11345  seqshft2  11349  monoord  11353  seqsplit  11356  seqf1o  11364  seqhomo  11370  faclbnd4lem4  11587  hasheqf1oi  11635  hashgt0elex  11670  hash1snb  11681  hashf1lem2  11705  hashf1  11706  seqcoll  11712  resqrex  12056  rexuz3  12152  rexanuz2  12153  limsupgre  12275  rlimconst  12338  caurcvg  12470  caucvg  12472  sumss  12518  fsumcl2lem  12525  fsumrlim  12590  fsumo1  12591  nn0seqcvgd  13061  exprmfct  13110  rpexp1i  13121  pcz  13254  pcadd  13258  pcmptcl  13260  prmlem0  13428  ressress  13526  sylow1lem1  15232  efgsf  15361  efgrelexlema  15381  dprdss  15587  ablfac1eulem  15630  lssssr  16029  psrvscafval  16454  mplcoe1  16528  mplcoe2  16530  epttop  17073  neiptopnei  17196  cmpsublem  17462  fiuncmp  17467  1stcrest  17516  kgenss  17575  hmeofval  17790  fbun  17872  fgss2  17906  filcon  17915  filuni  17917  filssufilg  17943  filufint  17952  hausflimi  18012  hausflim  18013  hauspwpwf1  18019  fclscmp  18062  alexsubALTlem4  18081  ptcmplem3  18085  ptcmplem5  18087  cstucnd  18314  isxmet2d  18357  imasdsf1olem  18403  blfps  18436  blf  18437  metrest  18554  nrginvrcn  18727  nmoge0  18755  nmoleub  18765  fsumcn  18900  cmetcaulem  19241  iscmet3  19246  iscmet2  19247  bcthlem2  19278  ovolicc2lem3  19415  itg2seq  19634  itg2splitlem  19640  itgeq1f  19663  itgeq2  19669  iblcnlem  19680  itgfsum  19718  limcnlp  19765  perfdvf  19790  dvnres  19817  dvmptfsum  19859  c1lip1  19881  mpfrcl  19939  aalioulem5  20253  abelth  20357  sinq12ge0  20416  rlimcnp  20804  xrlimcnp  20807  jensen  20827  ppiublem1  20986  dchrelbas3  21022  bcmono  21061  lgsquad2lem2  21143  2sqlem10  21158  pntrsumbnd2  21261  pntpbnd1  21280  pntlem3  21303  ausisusgra  21380  usgraidx2v  21412  nbgra0nb  21441  nbgranself2  21448  nbgraf1olem3  21453  nbgraf1olem5  21455  nb3graprlem1  21460  nbcusgra  21472  cusgrasizeinds  21485  uvtxnbgra  21502  wlkdvspthlem  21607  fargshiftfo  21625  3v3e3cycl1  21631  4cycl4v4e  21653  4cycl4dv4e  21655  vdgrf  21669  eupai  21689  eupath2  21702  isexid2  21913  zerdivemp1  22022  shsvs  22825  0cnop  23482  0cnfn  23483  cnlnssadj  23583  ssmd1  23814  ssmd2  23815  atexch  23884  mdsymlem4  23909  sumdmdlem  23921  ifeqeqx  24001  fmptcof2  24076  pwsiga  24513  subfacp1lem6  24871  erdszelem8  24884  cvmliftlem7  24978  cvmliftlem10  24981  cvmlift2lem12  25001  dedekind  25187  fprodcl2lem  25276  trpredlem1  25505  poseq  25528  funpartfv  25790  axlowdimlem15  25895  axcontlem7  25909  endofsegid  26019  broutsideof2  26056  ordcmp  26197  findreccl  26203  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  itg2addnclem3  26258  itg2addnc  26259  ftc1anc  26288  areacirclem1  26292  a1i13  26298  a1i24  26301  nn0prpwlem  26325  nn0prpw  26326  sdclem2  26446  fdc  26449  mettrifi  26463  zerdivemp1x  26571  smprngopr  26662  jca3  26693  monotoddzzfi  27005  psgnunilem4  27397  refsum2cnlem1  27684  stoweidlem31  27756  reuan  27934  2reu4  27944  funressnfv  27968  ndmaovass  28046  otsndisj  28065  otiunsndisj  28066  otiunsndisjX  28067  fzoopth  28139  euhash1  28167  swrdnd  28182  swrdvalodm2  28188  swrdswrd  28199  swrdccatin1  28205  swrdccatin12lem4  28213  swrdccat3  28215  swrdccat3blem  28218  cshwcl  28240  2cshwmod  28257  cshw1  28275  cshwssizelem1a  28279  cshwssizelem2  28281  cshwssizelem4a  28283  cshwsdisj  28285  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2pth  28311  el2wlkonotot0  28339  usg2wlkonot  28350  usg2wotspth  28351  2spontn0vne  28354  frgra2v  28389  frgra3vlem1  28390  3vfriswmgralem  28394  1to2vfriswmgra  28396  1to3vfriswmgra  28397  2pthfrgra  28401  frgranbnb  28410  vdfrgra0  28412  vdgfrgra0  28413  vdn1frgrav2  28416  vdgn1frgrav2  28417  vdgfrgragt2  28418  frgrawopreglem2  28434  frgrawopreglem3  28435  frgrawopreglem4  28436  frgrawopreg  28438  frgraregorufr0  28441  frgraregorufr  28442  2spotdisj  28450  2spotiundisj  28451  2spotmdisj  28457  ad4ant14  28539  ad4ant134  28542  ee121  28587  ee122  28588  rspsbc2  28618  a9e2ndeq  28646  vd12  28701  vd13  28702  ee221  28751  ee212  28753  ee112  28756  ee211  28759  ee210  28761  ee201  28763  ee120  28765  ee021  28767  ee012  28769  ee102  28771  ee03  28853  ee31  28864  ee31an  28866  ee123  28875  a9e2ndeqVD  29021  a9e2ndeqALT  29043  bnj151  29248  bnj594  29283  bnj600  29290  dvelimvNEW7  29462  equsalNEW7  29487  dvelimhvAUX7  29492  equviniNEW7  29527  equveliNEW7  29528  ax11vNEW7  29595  sbal1NEW7  29615  dvelimALTNEW7  29636  dvelimhOLD7  29713  lfl1dim  29919  lfl1dim2N  29920  lkreqN  29968  cvrexchlem  30216  ps-2  30275  paddasslem14  30630  idldil  30911  isltrn2N  30917  cdleme25a  31150  dibglbN  31964  dihlsscpre  32032  dvh4dimlem  32241  lcfl7N  32299  mapdval2N  32428
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator