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 4645 vs. uniexg 4646. (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  1851  equsalOLD  1955  dvelimvOLD  1985  dvelimh  2003  equvini  2022  equveli  2023  ax11v  2129  sbal1  2160  dvelimALT  2167  ax11  2189  hbequid  2194  dvelimf-o  2214  ax11eq  2227  ax11el  2228  ax11indalem  2231  ax11inda2ALT  2232  ax11inda2  2233  euan  2295  moexex  2307  rgen2a  2715  ralrimivw  2733  reximdv  2760  rexlimdvw  2776  reuind  3080  rexn0  3673  tppreqb  3882  prnebg  3921  axsep  4270  dtru  4331  fr0  4502  ordsssuc2  4610  reusv6OLD  4674  reusv7OLD  4675  ordsucelsuc  4742  tfinds  4779  tfindsg  4780  limomss  4790  findsg  4812  finds1  4814  ssrel2  4906  poltletr  5209  xpexr  5247  ndmfv  5695  fveqres  5703  fmptco  5840  elunirnALT  5939  ndmovord  6176  bropopvvv  6365  soxp  6395  mpt2xopynvov0  6405  smofvon2  6554  abianfplem  6651  oaordi  6725  oawordeulem  6733  odi  6758  brdomg  7054  map1  7121  fopwdom  7152  fodomr  7194  mapxpen  7209  infensuc  7221  onomeneq  7232  fineqvlem  7259  fineqv  7260  pssnn  7263  xpfi  7314  finsschain  7348  dffi3  7371  fisup2g  7404  fisupcl  7405  inf3lemd  7515  en3lplem2  7604  r1ordg  7637  r1val1  7645  r1pw  7704  r1pwOLD  7705  rankxplim3  7738  carddomi2  7790  fidomtri  7813  pr2ne  7822  alephon  7883  alephcard  7884  alephnbtwn  7885  alephordi  7888  iunfictbso  7928  fin23lem30  8155  fin1a2lem10  8222  domtriomlem  8255  axdc3lem2  8264  axdc3lem4  8266  alephval2  8380  cfpwsdom  8392  axextnd  8399  axrepnd  8402  axpownd  8409  axregnd  8412  axinfndlem1  8413  fpwwe2lem12  8449  wunfi  8529  addnidpi  8711  pinq  8737  ltexprlem7  8852  mulgt0sr  8913  nnind  9950  nn1m1nn  9952  nn0n0n1ge2b  10213  uzindOLD  10296  uzm1  10448  xrltnsym  10662  xrlttri  10664  xrlttr  10665  qbtwnxr  10718  xltnegi  10734  xlt2add  10771  xrsupsslem  10817  xrinfmsslem  10818  xrub  10822  fzospliti  11095  elfznelfzo  11119  injresinjlem  11126  injresinj  11127  seqfveq2  11272  seqshft2  11276  monoord  11280  seqsplit  11283  seqf1o  11291  seqhomo  11297  faclbnd4lem4  11514  hasheqf1oi  11562  hashgt0elex  11597  hash1snb  11608  hashf1lem2  11632  hashf1  11633  seqcoll  11639  resqrex  11983  rexuz3  12079  rexanuz2  12080  limsupgre  12202  rlimconst  12265  caurcvg  12397  caucvg  12399  sumss  12445  fsumcl2lem  12452  fsumrlim  12517  fsumo1  12518  nn0seqcvgd  12988  exprmfct  13037  rpexp1i  13048  pcz  13181  pcadd  13185  pcmptcl  13187  prmlem0  13355  ressress  13453  sylow1lem1  15159  efgsf  15288  efgrelexlema  15308  dprdss  15514  ablfac1eulem  15557  lssssr  15956  psrvscafval  16381  mplcoe1  16455  mplcoe2  16457  epttop  16996  neiptopnei  17119  cmpsublem  17384  fiuncmp  17389  1stcrest  17437  kgenss  17496  hmeofval  17711  fbun  17793  fgss2  17827  filcon  17836  filuni  17838  filssufilg  17864  filufint  17873  hausflimi  17933  hausflim  17934  hauspwpwf1  17940  fclscmp  17983  alexsubALTlem4  18002  ptcmplem3  18006  ptcmplem5  18008  cstucnd  18235  isxmet2d  18266  imasdsf1olem  18311  blf  18335  metrest  18444  nrginvrcn  18598  nmoge0  18626  nmoleub  18636  fsumcn  18771  cmetcaulem  19112  iscmet3  19117  iscmet2  19118  bcthlem2  19147  ovolicc2lem3  19282  itg2seq  19501  itg2splitlem  19507  itgeq1f  19530  itgeq2  19536  iblcnlem  19547  itgfsum  19585  limcnlp  19632  perfdvf  19657  dvnres  19684  dvmptfsum  19726  c1lip1  19748  mpfrcl  19806  aalioulem5  20120  abelth  20224  sinq12ge0  20283  rlimcnp  20671  xrlimcnp  20674  jensen  20694  ppiublem1  20853  dchrelbas3  20889  bcmono  20928  lgsquad2lem2  21010  2sqlem10  21025  pntrsumbnd2  21128  pntpbnd1  21147  pntlem3  21170  ausisusgra  21247  usgraidx2v  21278  nbusgra  21306  nbgra0nb  21307  nbgranself2  21314  nbgraf1olem3  21319  nbgraf1olem5  21321  nb3graprlem1  21326  nbcusgra  21338  cusgrasizeinds  21351  uvtxnbgra  21368  wlkdvspthlem  21455  fargshiftfo  21473  3v3e3cycl1  21479  4cycl4v4e  21501  4cycl4dv4e  21503  vdgrf  21517  eupai  21537  eupath2  21550  isexid2  21761  zerdivemp1  21870  shsvs  22673  0cnop  23330  0cnfn  23331  cnlnssadj  23431  ssmd1  23662  ssmd2  23663  atexch  23732  mdsymlem4  23757  sumdmdlem  23769  ifeqeqx  23845  fmptcof2  23918  pwsiga  24309  subfacp1lem6  24650  erdszelem8  24663  cvmliftlem7  24757  cvmliftlem10  24760  cvmlift2lem12  24780  dedekind  24966  fprodcl2lem  25055  trpredlem1  25254  poseq  25277  funpartfv  25508  axlowdimlem15  25609  axcontlem7  25623  endofsegid  25733  broutsideof2  25770  ordcmp  25911  findreccl  25917  ovoliunnfl  25953  voliunnfl  25955  volsupnfl  25956  itg2addnc  25959  areacirclem2  25982  a1i13  25989  a1i24  25992  nn0prpwlem  26016  nn0prpw  26017  sdclem2  26137  fdc  26140  mettrifi  26154  zerdivemp1x  26262  smprngopr  26353  jca3  26384  monotoddzzfi  26696  psgnunilem4  27089  refsum2cnlem1  27376  stoweidlem31  27448  reuan  27626  2reu4  27636  funressnfv  27661  ndmaovass  27739  frgra2v  27752  frgra3vlem1  27753  3vfriswmgralem  27757  1to2vfriswmgra  27759  1to3vfriswmgra  27760  2pthfrgra  27764  frgranbnb  27773  vdfrgra0  27775  vdgfrgra0  27776  vdn1frgrav2  27779  vdgn1frgrav2  27780  vdgfrgragt2  27781  frgrawopreglem2  27797  frgrawopreglem3  27798  frgrawopreglem4  27799  frgrawopreg  27801  frgraregorufr0  27804  frgraregorufr  27805  ad4ant14  27885  ad4ant134  27888  ee121  27930  ee122  27931  rspsbc2  27961  a9e2ndeq  27989  vd12  28042  vd13  28043  ee221  28092  ee212  28094  ee112  28097  ee211  28100  ee210  28102  ee201  28104  ee120  28106  ee021  28108  ee012  28110  ee102  28112  ee03  28194  ee31  28205  ee31an  28207  ee123  28216  a9e2ndeqVD  28362  a9e2ndeqALT  28385  bnj151  28586  bnj594  28621  bnj600  28628  dvelimvNEW7  28800  equsalNEW7  28825  dvelimhvAUX7  28830  equviniNEW7  28863  equveliNEW7  28864  ax11vNEW7  28928  sbal1NEW7  28948  dvelimALTNEW7  28969  dvelimhOLD7  29029  lfl1dim  29236  lfl1dim2N  29237  lkreqN  29285  cvrexchlem  29533  ps-2  29592  paddasslem14  29947  idldil  30228  isltrn2N  30234  cdleme25a  30467  dibglbN  31281  dihlsscpre  31349  dvh4dimlem  31558  lcfl7N  31616  mapdval2N  31745
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator