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 4407 vs. uniexg 4408. (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  687  anbi1d  688  3ecase  1291  ee21  1371  meredith  1400  ax12olem16  1650  ax10lem24  1673  hbequid  1687  equsal  1850  equsalh  1851  dvelimfALT  1853  dvelimf-o  1854  equvini  1879  equveli  1880  ax11  1941  ax11v  1990  sbal1  2086  dvelimALT  2094  ax11eq  2105  ax11el  2106  ax11indalem  2110  ax11inda2ALT  2111  ax11inda2  2112  euan  2170  moexex  2182  rgen2a  2571  ralrimivw  2589  reximdv  2616  rexlimdvw  2632  reuind  2903  rexn0  3462  axsep  4037  dtru  4095  fr0  4265  ordsssuc2  4374  reusv6OLD  4436  reusv7OLD  4437  ordsucelsuc  4504  tfinds  4541  tfindsg  4542  limomss  4552  findsg  4574  finds1  4576  poltletr  4985  xpexr  5021  fveqres  5412  fmptco  5543  elunirnALT  5631  ndmovord  5862  soxp  6080  smofvon2  6259  abianfplem  6356  oaordi  6430  oawordeulem  6438  odi  6463  brdomg  6758  map1  6824  fopwdom  6855  fodomr  6897  mapxpen  6912  infensuc  6924  onomeneq  6935  fineqvlem  6962  fineqv  6963  pssnn  6966  xpfi  7013  finsschain  7046  dffi3  7068  fisup2g  7101  fisupcl  7102  inf3lemd  7212  en3lplem2  7301  r1ordg  7334  r1val1  7342  r1pw  7401  r1pwOLD  7402  rankxplim3  7435  carddomi2  7487  fidomtri  7510  pr2ne  7519  alephon  7580  alephcard  7581  alephnbtwn  7582  alephordi  7585  iunfictbso  7625  fin23lem30  7852  fin1a2lem10  7919  domtriomlem  7952  axdc3lem2  7961  axdc3lem4  7963  alephval2  8074  cfpwsdom  8086  axextnd  8093  axrepnd  8096  axpownd  8103  axregnd  8106  axinfndlem1  8107  fpwwe2lem12  8143  wunfi  8223  addnidpi  8405  pinq  8431  ltexprlem7  8546  mulgt0sr  8607  lbinfm  9587  nnind  9644  nn1m1nn  9646  uzindOLD  9985  uzm1  10137  xrltnsym  10350  xrlttri  10352  xrlttr  10353  qbtwnxr  10405  xltnegi  10421  xlt2add  10458  xrsupsslem  10503  xrinfmsslem  10504  xrub  10508  fzospliti  10776  seqfveq2  10946  seqshft2  10950  monoord  10954  seqsplit  10957  seqf1o  10965  seqhomo  10971  faclbnd4lem4  11187  hashf1lem2  11271  hashf1  11272  seqcoll  11278  resqrex  11613  rexuz3  11709  rexanuz2  11710  limsupgre  11832  rlimconst  11895  caurcvg  12026  caucvg  12028  sumss  12074  fsumcl2lem  12081  fsumrlim  12146  fsumo1  12147  nn0seqcvgd  12614  exprmfct  12663  rpexp1i  12674  pcz  12807  pcadd  12811  pcmptcl  12813  prmlem0  12981  ressress  13079  sylow1lem1  14744  efgsf  14873  efgrelexlema  14893  dprdss  15099  dprdsn  15106  ablfac1eulem  15142  lssssr  15545  psrvscafval  15967  mplcoe1  16041  mplcoe2  16043  epttop  16578  cmpsublem  16958  fiuncmp  16963  1stcrest  17011  kgenss  17070  hmeofval  17281  fbun  17367  fgss2  17401  filcon  17410  filuni  17412  filssufilg  17438  filufint  17447  hausflimi  17507  hausflim  17508  hauspwpwf1  17514  fclscmp  17557  alexsubALTlem4  17576  ptcmplem3  17580  ptcmplem5  17582  isxmet2d  17724  imasdsf1olem  17769  blf  17793  metrest  17902  nrginvrcn  18034  nmoge0  18062  nmoleub  18072  fsumcn  18206  cmetcaulem  18546  iscmet3  18551  iscmet2  18552  bcthlem2  18579  ovolicc2lem3  18710  itg2seq  18929  itg2splitlem  18935  itgeq1f  18958  itgeq2  18964  iblcnlem  18975  itgfsum  19013  limcnlp  19060  perfdvf  19085  dvnres  19112  dvmptfsum  19154  c1lip1  19176  mpfrcl  19234  aalioulem5  19548  abelth  19649  sinq12ge0  19708  rlimcnp  20092  xrlimcnp  20095  jensen  20115  ppiublem1  20273  dchrelbas3  20309  bcmono  20348  lgsquad2lem2  20430  2sqlem10  20445  pntrsumbnd2  20548  pntpbnd1  20567  pntlem3  20590  isexid2  20822  shsvs  21732  0cnop  22389  0cnfn  22390  cnlnssadj  22490  ssmd1  22721  ssmd2  22722  atexch  22791  mdsymlem4  22816  sumdmdlem  22828  subfacp1lem6  22887  erdszelem8  22900  cvmliftlem7  22993  cvmliftlem10  22996  cvmlift2lem12  23016  eupai  23054  eupath2  23075  dedekind  23252  trpredlem1  23398  poseq  23421  axlowdimlem15  23758  axcontlem7  23772  endofsegid  23882  broutsideof2  23919  ordcmp  24060  findreccl  24066  twsymr  24243  eqfnung2  24284  cbcpcp  24328  prl  24333  oriso  24380  dupre1  24409  fsumprd  24495  multinvb  24589  zerdivemp1  24602  svli2  24650  svs3  24654  efilcp  24718  islimrs3  24747  sigadd  24815  clsmulcv  24848  distmlva  24854  intvconlem1  24869  cmpassoh  24967  prismorcsetlemc  25083  domcatfun  25091  gltpntl  25238  lineval4a  25253  isconcl6ab  25270  xsyysx  25311  bsstrs  25312  nbssntrs  25313  a1i13  25366  a1i24  25369  nn0prpwlem  25404  nn0prpw  25405  sdclem2  25618  fdc  25621  mettrifi  25639  zerdivemp1x  25752  smprngopr  25843  jca3  25876  prtlem80  25890  monotoddzzfi  26193  psgnunilem4  26586  ee121  26959  ee122  26960  ra4sbc2  26990  a9e2ndeq  27018  vd12  27062  vd13  27063  ee221  27112  ee212  27114  ee112  27117  ee211  27120  ee210  27122  ee201  27124  ee120  27126  ee021  27128  ee012  27130  ee102  27132  ee03  27206  ee31  27217  ee31an  27219  ee123  27228  a9e2ndeqVD  27375  a9e2ndeqALT  27398  bnj151  27598  bnj594  27633  bnj600  27640  ax10lem17ALT  27812  a12lem1  27819  ax9lem17  27845  lfl1dim  28000  lfl1dim2N  28001  lkreqN  28049  cvrexchlem  28297  ps-2  28356  paddasslem14  28711  idldil  28992  isltrn2N  28998  cdleme25a  29231  dibglbN  30045  dihlsscpre  30113  dvh4dimlem  30322  lcfl7N  30380  mapdval2N  30509
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator