MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1d 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 12. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 7. 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 4517 vs. uniexg 4518. (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 7 . 2  |-  ( ps 
->  ( ch  ->  ps ) )
31, 2syl 17 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  a1ii  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  184  imbi2d  309  adantr  453  jctild  529  jctird  530  pm3.4  546  anbi2d  686  anbi1d  687  3ecase  1288  ee21  1367  meredith  1396  equsalhw  1734  dvelimv  1883  equsal  1905  dvelimfALT  1909  equvini  1932  equveli  1933  ax11v  2038  sbal1  2070  dvelimALT  2077  ax11  2098  hbequid  2103  dvelimf-o  2123  ax11eq  2135  ax11el  2136  ax11indalem  2139  ax11inda2ALT  2140  ax11inda2  2141  euan  2203  moexex  2215  rgen2a  2612  ralrimivw  2630  reximdv  2657  rexlimdvw  2673  reuind  2971  rexn0  3559  axsep  4143  dtru  4202  fr0  4373  ordsssuc2  4482  reusv6OLD  4546  reusv7OLD  4547  ordsucelsuc  4614  tfinds  4651  tfindsg  4652  limomss  4662  findsg  4684  finds1  4686  poltletr  5079  xpexr  5115  fveqres  5523  fmptco  5654  elunirnALT  5742  ndmovord  5973  soxp  6191  smofvon2  6370  abianfplem  6467  oaordi  6541  oawordeulem  6549  odi  6574  brdomg  6869  map1  6936  fopwdom  6967  fodomr  7009  mapxpen  7024  infensuc  7036  onomeneq  7047  fineqvlem  7074  fineqv  7075  pssnn  7078  xpfi  7125  finsschain  7159  dffi3  7181  fisup2g  7214  fisupcl  7215  inf3lemd  7325  en3lplem2  7414  r1ordg  7447  r1val1  7455  r1pw  7514  r1pwOLD  7515  rankxplim3  7548  carddomi2  7600  fidomtri  7623  pr2ne  7632  alephon  7693  alephcard  7694  alephnbtwn  7695  alephordi  7698  iunfictbso  7738  fin23lem30  7965  fin1a2lem10  8032  domtriomlem  8065  axdc3lem2  8074  axdc3lem4  8076  alephval2  8191  cfpwsdom  8203  axextnd  8210  axrepnd  8213  axpownd  8220  axregnd  8223  axinfndlem1  8224  fpwwe2lem12  8260  wunfi  8340  addnidpi  8522  pinq  8548  ltexprlem7  8663  mulgt0sr  8724  lbinfm  9704  nnind  9761  nn1m1nn  9763  uzindOLD  10103  uzm1  10255  xrltnsym  10468  xrlttri  10470  xrlttr  10471  qbtwnxr  10523  xltnegi  10539  xlt2add  10576  xrsupsslem  10621  xrinfmsslem  10622  xrub  10626  fzospliti  10894  seqfveq2  11064  seqshft2  11068  monoord  11072  seqsplit  11075  seqf1o  11083  seqhomo  11089  faclbnd4lem4  11305  hashf1lem2  11390  hashf1  11391  seqcoll  11397  resqrex  11732  rexuz3  11828  rexanuz2  11829  limsupgre  11951  rlimconst  12014  caurcvg  12145  caucvg  12147  sumss  12193  fsumcl2lem  12200  fsumrlim  12265  fsumo1  12266  nn0seqcvgd  12736  exprmfct  12785  rpexp1i  12796  pcz  12929  pcadd  12933  pcmptcl  12935  prmlem0  13103  ressress  13201  sylow1lem1  14905  efgsf  15034  efgrelexlema  15054  dprdss  15260  dprdsn  15267  ablfac1eulem  15303  lssssr  15706  psrvscafval  16131  mplcoe1  16205  mplcoe2  16207  epttop  16742  cmpsublem  17122  fiuncmp  17127  1stcrest  17175  kgenss  17234  hmeofval  17445  fbun  17531  fgss2  17565  filcon  17574  filuni  17576  filssufilg  17602  filufint  17611  hausflimi  17671  hausflim  17672  hauspwpwf1  17678  fclscmp  17721  alexsubALTlem4  17740  ptcmplem3  17744  ptcmplem5  17746  isxmet2d  17888  imasdsf1olem  17933  blf  17957  metrest  18066  nrginvrcn  18198  nmoge0  18226  nmoleub  18236  fsumcn  18370  cmetcaulem  18710  iscmet3  18715  iscmet2  18716  bcthlem2  18743  ovolicc2lem3  18874  itg2seq  19093  itg2splitlem  19099  itgeq1f  19122  itgeq2  19128  iblcnlem  19139  itgfsum  19177  limcnlp  19224  perfdvf  19249  dvnres  19276  dvmptfsum  19318  c1lip1  19340  mpfrcl  19398  aalioulem5  19712  abelth  19813  sinq12ge0  19872  rlimcnp  20256  xrlimcnp  20259  jensen  20279  ppiublem1  20437  dchrelbas3  20473  bcmono  20512  lgsquad2lem2  20594  2sqlem10  20609  pntrsumbnd2  20712  pntpbnd1  20731  pntlem3  20754  isexid2  20986  shsvs  21896  0cnop  22553  0cnfn  22554  cnlnssadj  22654  ssmd1  22885  ssmd2  22886  atexch  22955  mdsymlem4  22980  sumdmdlem  22992  ifeqeqx  23028  subfacp1lem6  23122  erdszelem8  23135  cvmliftlem7  23228  cvmliftlem10  23231  cvmlift2lem12  23251  eupai  23289  eupath2  23310  dedekind  23487  trpredlem1  23633  poseq  23656  axlowdimlem15  23993  axcontlem7  24007  endofsegid  24117  broutsideof2  24154  ordcmp  24295  findreccl  24301  twsymr  24478  eqfnung2  24519  cbcpcp  24563  prl  24568  oriso  24615  dupre1  24644  fsumprd  24730  multinvb  24824  zerdivemp1  24837  svli2  24885  svs3  24889  efilcp  24953  islimrs3  24982  sigadd  25050  clsmulcv  25083  distmlva  25089  intvconlem1  25104  cmpassoh  25202  prismorcsetlemc  25318  domcatfun  25326  gltpntl  25473  lineval4a  25488  isconcl6ab  25505  xsyysx  25546  bsstrs  25547  nbssntrs  25548  a1i13  25601  a1i24  25604  nn0prpwlem  25639  nn0prpw  25640  sdclem2  25853  fdc  25856  mettrifi  25874  zerdivemp1x  25987  smprngopr  26078  jca3  26111  prtlem80  26125  monotoddzzfi  26428  psgnunilem4  26821  fsumcnf  27093  refsum2cnlem1  27109  stoweidlem29  27179  stoweidlem31  27181  stoweidlem35  27185  reuan  27339  2reu4  27349  funressnfv  27372  ndmaovass  27447  ee121  27539  ee122  27540  rspsbc2  27570  a9e2ndeq  27598  vd12  27642  vd13  27643  ee221  27692  ee212  27694  ee112  27697  ee211  27700  ee210  27702  ee201  27704  ee120  27706  ee021  27708  ee012  27710  ee102  27712  ee03  27786  ee31  27797  ee31an  27799  ee123  27808  a9e2ndeqVD  27955  a9e2ndeqALT  27978  bnj151  28178  bnj594  28213  bnj600  28220  ax10lem17ALT  28392  a12lem1  28399  ax9lem17  28425  lfl1dim  28580  lfl1dim2N  28581  lkreqN  28629  cvrexchlem  28877  ps-2  28936  paddasslem14  29291  idldil  29572  isltrn2N  29578  cdleme25a  29811  dibglbN  30625  dihlsscpre  30693  dvh4dimlem  30902  lcfl7N  30960  mapdval2N  31089
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator