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

Theorem a1d 22
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 360) 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 10. 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 47 vs. pm2.43i 43 vs. pm2.43d 44). 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 4532 vs. uniexg 4533. (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 15 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  a1ii  24  syl5com  26  mpid  37  syld  40  imim2d  48  syl5d  62  syl6d  64  pm2.21d  98  pm2.24d  135  pm2.51  145  pm2.521  146  pm2.61iii  159  mtod  168  impbid21d  182  imbi2d  307  adantr  451  jctild  527  jctird  528  pm3.4  544  anbi2d  684  anbi1d  685  3ecase  1286  ee21  1365  meredith  1394  equsalhw  1742  dvelimv  1892  equsal  1913  dvelimh  1917  equvini  1940  equveli  1941  ax11v  2049  sbal1  2078  dvelimALT  2085  ax11  2107  hbequid  2112  dvelimf-o  2132  ax11eq  2145  ax11el  2146  ax11indalem  2149  ax11inda2ALT  2150  ax11inda2  2151  euan  2213  moexex  2225  rgen2a  2622  ralrimivw  2640  reximdv  2667  rexlimdvw  2683  reuind  2981  rexn0  3569  axsep  4156  dtru  4217  fr0  4388  ordsssuc2  4497  reusv6OLD  4561  reusv7OLD  4562  ordsucelsuc  4629  tfinds  4666  tfindsg  4667  limomss  4677  findsg  4699  finds1  4701  poltletr  5094  xpexr  5130  ndmfv  5568  fveqres  5576  fmptco  5707  elunirnALT  5795  ndmovord  6026  soxp  6244  smofvon2  6389  abianfplem  6486  oaordi  6560  oawordeulem  6568  odi  6593  brdomg  6888  map1  6955  fopwdom  6986  fodomr  7028  mapxpen  7043  infensuc  7055  onomeneq  7066  fineqvlem  7093  fineqv  7094  pssnn  7097  xpfi  7144  finsschain  7178  dffi3  7200  fisup2g  7233  fisupcl  7234  inf3lemd  7344  en3lplem2  7433  r1ordg  7466  r1val1  7474  r1pw  7533  r1pwOLD  7534  rankxplim3  7567  carddomi2  7619  fidomtri  7642  pr2ne  7651  alephon  7712  alephcard  7713  alephnbtwn  7714  alephordi  7717  iunfictbso  7757  fin23lem30  7984  fin1a2lem10  8051  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  alephval2  8210  cfpwsdom  8222  axextnd  8229  axrepnd  8232  axpownd  8239  axregnd  8242  axinfndlem1  8243  fpwwe2lem12  8279  wunfi  8359  addnidpi  8541  pinq  8567  ltexprlem7  8682  mulgt0sr  8743  lbinfm  9723  nnind  9780  nn1m1nn  9782  uzindOLD  10122  uzm1  10274  xrltnsym  10487  xrlttri  10489  xrlttr  10490  qbtwnxr  10543  xltnegi  10559  xlt2add  10596  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  fzospliti  10914  seqfveq2  11084  seqshft2  11088  monoord  11092  seqsplit  11095  seqf1o  11103  seqhomo  11109  faclbnd4lem4  11325  hashf1lem2  11410  hashf1  11411  seqcoll  11417  resqrex  11752  rexuz3  11848  rexanuz2  11849  limsupgre  11971  rlimconst  12034  caurcvg  12165  caucvg  12167  sumss  12213  fsumcl2lem  12220  fsumrlim  12285  fsumo1  12286  nn0seqcvgd  12756  exprmfct  12805  rpexp1i  12816  pcz  12949  pcadd  12953  pcmptcl  12955  prmlem0  13123  ressress  13221  sylow1lem1  14925  efgsf  15054  efgrelexlema  15074  dprdss  15280  dprdsn  15287  ablfac1eulem  15323  lssssr  15726  psrvscafval  16151  mplcoe1  16225  mplcoe2  16227  epttop  16762  cmpsublem  17142  fiuncmp  17147  1stcrest  17195  kgenss  17254  hmeofval  17465  fbun  17551  fgss2  17585  filcon  17594  filuni  17596  filssufilg  17622  filufint  17631  hausflimi  17691  hausflim  17692  hauspwpwf1  17698  fclscmp  17741  alexsubALTlem4  17760  ptcmplem3  17764  ptcmplem5  17766  isxmet2d  17908  imasdsf1olem  17953  blf  17977  metrest  18086  nrginvrcn  18218  nmoge0  18246  nmoleub  18256  fsumcn  18390  cmetcaulem  18730  iscmet3  18735  iscmet2  18736  bcthlem2  18763  ovolicc2lem3  18894  itg2seq  19113  itg2splitlem  19119  itgeq1f  19142  itgeq2  19148  iblcnlem  19159  itgfsum  19197  limcnlp  19244  perfdvf  19269  dvnres  19296  dvmptfsum  19338  c1lip1  19360  mpfrcl  19418  aalioulem5  19732  abelth  19833  sinq12ge0  19892  rlimcnp  20276  xrlimcnp  20279  jensen  20299  ppiublem1  20457  dchrelbas3  20493  bcmono  20532  lgsquad2lem2  20614  2sqlem10  20629  pntrsumbnd2  20732  pntpbnd1  20751  pntlem3  20774  isexid2  21008  shsvs  21918  0cnop  22575  0cnfn  22576  cnlnssadj  22676  ssmd1  22907  ssmd2  22908  atexch  22977  mdsymlem4  23002  sumdmdlem  23014  ifeqeqx  23050  xppreima  23226  fmptcof2  23244  pwsiga  23506  subfacp1lem6  23731  erdszelem8  23744  cvmliftlem7  23837  cvmliftlem10  23840  cvmlift2lem12  23860  eupai  23898  eupath2  23919  dedekind  24097  trpredlem1  24301  poseq  24324  funpartfv  24555  axlowdimlem15  24656  axcontlem7  24670  endofsegid  24780  broutsideof2  24817  ordcmp  24958  findreccl  24964  ovoliunnfl  25001  itg2addnc  25005  areacirclem2  25028  twsymr  25181  eqfnung2  25221  cbcpcp  25265  prl  25270  oriso  25317  dupre1  25346  fsumprd  25432  multinvb  25526  zerdivemp1  25539  svli2  25587  svs3  25591  efilcp  25655  islimrs3  25684  sigadd  25752  clsmulcv  25785  distmlva  25791  intvconlem1  25806  cmpassoh  25904  prismorcsetlemc  26020  domcatfun  26028  gltpntl  26175  lineval4a  26190  isconcl6ab  26207  xsyysx  26248  bsstrs  26249  nbssntrs  26250  a1i13  26303  a1i24  26306  nn0prpwlem  26341  nn0prpw  26342  sdclem2  26555  fdc  26558  mettrifi  26576  zerdivemp1x  26689  smprngopr  26780  jca3  26813  prtlem80  26827  monotoddzzfi  27130  psgnunilem4  27523  fsumcnf  27795  refsum2cnlem1  27811  stoweidlem29  27881  stoweidlem31  27883  stoweidlem35  27887  reuan  28061  2reu4  28071  funressnfv  28096  ndmaovass  28174  mpt2xopynvov0  28200  elfznelfzo  28213  injresinjlem  28214  injresinj  28215  nbusgra  28277  nbgra0nb  28278  nbgranself2  28285  nb3graprlem1  28287  nbcusgra  28298  uvtxnbgra  28306  trlonprop  28341  wlkdvspthlem  28365  fargshiftfo  28383  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  frgra2v  28423  frgra3vlem1  28424  3vfriswmgralem  28428  1to2vfriswmgra  28430  1to3vfriswmgra  28431  ad4ant14  28520  ad4ant134  28523  ad5ant1345  28543  ee121  28565  ee122  28566  rspsbc2  28596  a9e2ndeq  28624  vd12  28677  vd13  28678  ee221  28727  ee212  28729  ee112  28732  ee211  28735  ee210  28737  ee201  28739  ee120  28741  ee021  28743  ee012  28745  ee102  28747  ee03  28830  ee31  28841  ee31an  28843  ee123  28852  a9e2ndeqVD  29001  a9e2ndeqALT  29024  bnj151  29225  bnj594  29260  bnj600  29267  dvelimvNEW7  29439  equsalNEW7  29464  dvelimhvAUX7  29469  equviniNEW7  29502  equveliNEW7  29503  ax11vNEW7  29567  sbal1NEW7  29587  dvelimhOLD7  29667  ax10lem17ALT  29745  a12lem1  29752  ax9lem17  29778  lfl1dim  29933  lfl1dim2N  29934  lkreqN  29982  cvrexchlem  30230  ps-2  30289  paddasslem14  30644  idldil  30925  isltrn2N  30931  cdleme25a  31164  dibglbN  31978  dihlsscpre  32046  dvh4dimlem  32255  lcfl7N  32313  mapdval2N  32442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator