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

Theorem a1d 24
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 362) 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 50 vs. pm2.43i 46 vs. pm2.43d 47). 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 4706 vs. uniexg 4707. (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  27  syl5com  29  mpid  40  syld  43  imim2d  51  syl5d  65  syl6d  67  pm2.21d  101  pm2.24d  138  pm2.51  148  pm2.521  149  pm2.61iii  162  mtod  171  impbid21d  184  imbi2d  309  adantr  453  jctild  529  jctird  530  pm3.4  546  anbi2d  686  anbi1d  687  3ecase  1289  ee21  1385  meredith  1414  equsalhwOLD  1862  equsalOLD  2001  dvelimvOLD  2029  dvelimhOLD  2073  equviniOLD  2085  equveliOLD  2087  nfsb4t  2128  ax11v  2173  sbal1  2204  dvelimALT  2211  ax11  2233  hbequid  2238  dvelimf-o  2258  ax11eq  2271  ax11el  2272  ax11indalem  2275  ax11inda2ALT  2276  ax11inda2  2277  euan  2339  moexex  2351  rgen2a  2773  ralrimivw  2791  reximdv  2818  rexlimdvw  2834  reuind  3138  rexn0  3731  tppreqb  3940  prnebg  3980  axsep  4330  dtru  4391  fr0  4562  ordsssuc2  4671  reusv6OLD  4735  reusv7OLD  4736  ordsucelsuc  4803  tfinds  4840  tfindsg  4841  limomss  4851  findsg  4873  finds1  4875  ssrel2  4967  poltletr  5270  xpexr  5308  ndmfv  5756  fveqres  5765  fmptco  5902  elunirnALT  6001  ndmovord  6238  bropopvvv  6427  soxp  6460  mpt2xopynvov0  6470  smofvon2  6619  abianfplem  6716  oaordi  6790  oawordeulem  6798  odi  6823  brdomg  7119  map1  7186  fopwdom  7217  fodomr  7259  mapxpen  7274  infensuc  7286  onomeneq  7297  fineqvlem  7324  fineqv  7325  pssnn  7328  xpfi  7379  finsschain  7414  dffi3  7437  fisup2g  7472  fisupcl  7473  inf3lemd  7583  en3lplem2  7672  r1ordg  7705  r1val1  7713  r1pw  7772  r1pwOLD  7773  rankxplim3  7806  carddomi2  7858  fidomtri  7881  pr2ne  7890  alephon  7951  alephcard  7952  alephnbtwn  7953  alephordi  7956  iunfictbso  7996  fin23lem30  8223  fin1a2lem10  8290  domtriomlem  8323  axdc3lem2  8332  axdc3lem4  8334  alephval2  8448  cfpwsdom  8460  axextnd  8467  axrepnd  8470  axpownd  8477  axregnd  8480  axinfndlem1  8481  fpwwe2lem12  8517  wunfi  8597  addnidpi  8779  pinq  8805  ltexprlem7  8920  mulgt0sr  8981  nnind  10019  nn1m1nn  10021  nn0n0n1ge2b  10282  uzindOLD  10365  uzm1  10517  xrltnsym  10731  xrlttri  10733  xrlttr  10734  qbtwnxr  10787  xltnegi  10803  xlt2add  10840  xrsupsslem  10886  xrinfmsslem  10887  xrub  10891  fzospliti  11166  elfznelfzo  11193  injresinjlem  11200  injresinj  11201  seqfveq2  11346  seqshft2  11350  monoord  11354  seqsplit  11357  seqf1o  11365  seqhomo  11371  faclbnd4lem4  11588  hasheqf1oi  11636  hashgt0elex  11671  hash1snb  11682  hashf1lem2  11706  hashf1  11707  seqcoll  11713  resqrex  12057  rexuz3  12153  rexanuz2  12154  limsupgre  12276  rlimconst  12339  caurcvg  12471  caucvg  12473  sumss  12519  fsumcl2lem  12526  fsumrlim  12591  fsumo1  12592  nn0seqcvgd  13062  exprmfct  13111  rpexp1i  13122  pcz  13255  pcadd  13259  pcmptcl  13261  prmlem0  13429  ressress  13527  sylow1lem1  15233  efgsf  15362  efgrelexlema  15382  dprdss  15588  ablfac1eulem  15631  lssssr  16030  psrvscafval  16455  mplcoe1  16529  mplcoe2  16531  epttop  17074  neiptopnei  17197  cmpsublem  17463  fiuncmp  17468  1stcrest  17517  kgenss  17576  hmeofval  17791  fbun  17873  fgss2  17907  filcon  17916  filuni  17918  filssufilg  17944  filufint  17953  hausflimi  18013  hausflim  18014  hauspwpwf1  18020  fclscmp  18063  alexsubALTlem4  18082  ptcmplem3  18086  ptcmplem5  18088  cstucnd  18315  isxmet2d  18358  imasdsf1olem  18404  blfps  18437  blf  18438  metrest  18555  nrginvrcn  18728  nmoge0  18756  nmoleub  18766  fsumcn  18901  cmetcaulem  19242  iscmet3  19247  iscmet2  19248  bcthlem2  19279  ovolicc2lem3  19416  itg2seq  19635  itg2splitlem  19641  itgeq1f  19664  itgeq2  19670  iblcnlem  19681  itgfsum  19719  limcnlp  19766  perfdvf  19791  dvnres  19818  dvmptfsum  19860  c1lip1  19882  mpfrcl  19940  aalioulem5  20254  abelth  20358  sinq12ge0  20417  rlimcnp  20805  xrlimcnp  20808  jensen  20828  ppiublem1  20987  dchrelbas3  21023  bcmono  21062  lgsquad2lem2  21144  2sqlem10  21159  pntrsumbnd2  21262  pntpbnd1  21281  pntlem3  21304  ausisusgra  21381  usgraidx2v  21413  nbgra0nb  21442  nbgranself2  21449  nbgraf1olem3  21454  nbgraf1olem5  21456  nb3graprlem1  21461  nbcusgra  21473  cusgrasizeinds  21486  uvtxnbgra  21503  wlkdvspthlem  21608  fargshiftfo  21626  3v3e3cycl1  21632  4cycl4v4e  21654  4cycl4dv4e  21656  vdgrf  21670  eupai  21690  eupath2  21703  isexid2  21914  zerdivemp1  22023  shsvs  22826  0cnop  23483  0cnfn  23484  cnlnssadj  23584  ssmd1  23815  ssmd2  23816  atexch  23885  mdsymlem4  23910  sumdmdlem  23922  ifeqeqx  24002  fmptcof2  24077  pwsiga  24514  subfacp1lem6  24872  erdszelem8  24885  cvmliftlem7  24979  cvmliftlem10  24982  cvmlift2lem12  25002  dedekind  25188  fprodcl2lem  25277  trpredlem1  25506  poseq  25529  funpartfv  25791  axlowdimlem15  25896  axcontlem7  25910  endofsegid  26020  broutsideof2  26057  ordcmp  26198  findreccl  26204  ovoliunnfl  26249  voliunnfl  26251  volsupnfl  26252  itg2addnclem3  26259  itg2addnc  26260  ftc1anc  26289  areacirclem1  26293  a1i13  26299  a1i24  26302  nn0prpwlem  26326  nn0prpw  26327  sdclem2  26447  fdc  26450  mettrifi  26464  zerdivemp1x  26572  smprngopr  26663  jca3  26694  monotoddzzfi  27006  psgnunilem4  27398  refsum2cnlem1  27685  stoweidlem31  27757  reuan  27935  2reu4  27945  funressnfv  27969  ndmaovass  28047  otsndisj  28066  otiunsndisj  28067  otiunsndisjX  28068  fzoopth  28140  euhash1  28168  swrdnd  28183  swrdvalodm2  28189  swrdswrd  28200  swrdccatin1  28206  swrdccatin12lem4  28214  swrdccat3  28216  swrdccat3blem  28219  cshwcl  28241  2cshwmod  28258  cshw1  28276  cshwssizelem1a  28280  cshwssizelem2  28282  cshwssizelem4a  28284  cshwsdisj  28286  usgra2pthspth  28306  usgra2wlkspthlem1  28307  usgra2pth  28312  el2wlkonotot0  28340  usg2wlkonot  28351  usg2wotspth  28352  2spontn0vne  28355  frgra2v  28390  frgra3vlem1  28391  3vfriswmgralem  28395  1to2vfriswmgra  28397  1to3vfriswmgra  28398  2pthfrgra  28402  frgranbnb  28411  vdfrgra0  28413  vdgfrgra0  28414  vdn1frgrav2  28417  vdgn1frgrav2  28418  vdgfrgragt2  28419  frgrawopreglem2  28435  frgrawopreglem3  28436  frgrawopreglem4  28437  frgrawopreg  28439  frgraregorufr0  28442  frgraregorufr  28443  2spotdisj  28451  2spotiundisj  28452  2spotmdisj  28458  ad4ant14  28540  ad4ant134  28543  ee121  28588  ee122  28589  rspsbc2  28619  a9e2ndeq  28647  vd12  28702  vd13  28703  ee221  28752  ee212  28754  ee112  28757  ee211  28760  ee210  28762  ee201  28764  ee120  28766  ee021  28768  ee012  28770  ee102  28772  ee03  28854  ee31  28865  ee31an  28867  ee123  28876  a9e2ndeqVD  29022  a9e2ndeqALT  29044  bnj151  29249  bnj594  29284  bnj600  29291  dvelimvNEW7  29463  equsalNEW7  29488  dvelimhvAUX7  29493  equviniNEW7  29528  equveliNEW7  29529  ax11vNEW7  29596  sbal1NEW7  29616  dvelimALTNEW7  29637  dvelimhOLD7  29714  lfl1dim  29920  lfl1dim2N  29921  lkreqN  29969  cvrexchlem  30217  ps-2  30276  paddasslem14  30631  idldil  30912  isltrn2N  30918  cdleme25a  31151  dibglbN  31965  dihlsscpre  32033  dvh4dimlem  32242  lcfl7N  32300  mapdval2N  32429
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator