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 4516 vs. uniexg 4517. (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  1730  dvelimv  1879  equsal  1900  dvelimh  1904  equvini  1927  equveli  1928  ax11v  2036  sbal1  2065  dvelimALT  2072  ax11  2094  hbequid  2099  dvelimf-o  2119  ax11eq  2132  ax11el  2133  ax11indalem  2136  ax11inda2ALT  2137  ax11inda2  2138  euan  2200  moexex  2212  rgen2a  2609  ralrimivw  2627  reximdv  2654  rexlimdvw  2670  reuind  2968  rexn0  3556  axsep  4140  dtru  4201  fr0  4372  ordsssuc2  4481  reusv6OLD  4545  reusv7OLD  4546  ordsucelsuc  4613  tfinds  4650  tfindsg  4651  limomss  4661  findsg  4683  finds1  4685  poltletr  5078  xpexr  5114  ndmfv  5552  fveqres  5560  fmptco  5691  elunirnALT  5779  ndmovord  6010  soxp  6228  smofvon2  6373  abianfplem  6470  oaordi  6544  oawordeulem  6552  odi  6577  brdomg  6872  map1  6939  fopwdom  6970  fodomr  7012  mapxpen  7027  infensuc  7039  onomeneq  7050  fineqvlem  7077  fineqv  7078  pssnn  7081  xpfi  7128  finsschain  7162  dffi3  7184  fisup2g  7217  fisupcl  7218  inf3lemd  7328  en3lplem2  7417  r1ordg  7450  r1val1  7458  r1pw  7517  r1pwOLD  7518  rankxplim3  7551  carddomi2  7603  fidomtri  7626  pr2ne  7635  alephon  7696  alephcard  7697  alephnbtwn  7698  alephordi  7701  iunfictbso  7741  fin23lem30  7968  fin1a2lem10  8035  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  alephval2  8194  cfpwsdom  8206  axextnd  8213  axrepnd  8216  axpownd  8223  axregnd  8226  axinfndlem1  8227  fpwwe2lem12  8263  wunfi  8343  addnidpi  8525  pinq  8551  ltexprlem7  8666  mulgt0sr  8727  lbinfm  9707  nnind  9764  nn1m1nn  9766  uzindOLD  10106  uzm1  10258  xrltnsym  10471  xrlttri  10473  xrlttr  10474  qbtwnxr  10527  xltnegi  10543  xlt2add  10580  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  fzospliti  10898  seqfveq2  11068  seqshft2  11072  monoord  11076  seqsplit  11079  seqf1o  11087  seqhomo  11093  faclbnd4lem4  11309  hashf1lem2  11394  hashf1  11395  seqcoll  11401  resqrex  11736  rexuz3  11832  rexanuz2  11833  limsupgre  11955  rlimconst  12018  caurcvg  12149  caucvg  12151  sumss  12197  fsumcl2lem  12204  fsumrlim  12269  fsumo1  12270  nn0seqcvgd  12740  exprmfct  12789  rpexp1i  12800  pcz  12933  pcadd  12937  pcmptcl  12939  prmlem0  13107  ressress  13205  sylow1lem1  14909  efgsf  15038  efgrelexlema  15058  dprdss  15264  dprdsn  15271  ablfac1eulem  15307  lssssr  15710  psrvscafval  16135  mplcoe1  16209  mplcoe2  16211  epttop  16746  cmpsublem  17126  fiuncmp  17131  1stcrest  17179  kgenss  17238  hmeofval  17449  fbun  17535  fgss2  17569  filcon  17578  filuni  17580  filssufilg  17606  filufint  17615  hausflimi  17675  hausflim  17676  hauspwpwf1  17682  fclscmp  17725  alexsubALTlem4  17744  ptcmplem3  17748  ptcmplem5  17750  isxmet2d  17892  imasdsf1olem  17937  blf  17961  metrest  18070  nrginvrcn  18202  nmoge0  18230  nmoleub  18240  fsumcn  18374  cmetcaulem  18714  iscmet3  18719  iscmet2  18720  bcthlem2  18747  ovolicc2lem3  18878  itg2seq  19097  itg2splitlem  19103  itgeq1f  19126  itgeq2  19132  iblcnlem  19143  itgfsum  19181  limcnlp  19228  perfdvf  19253  dvnres  19280  dvmptfsum  19322  c1lip1  19344  mpfrcl  19402  aalioulem5  19716  abelth  19817  sinq12ge0  19876  rlimcnp  20260  xrlimcnp  20263  jensen  20283  ppiublem1  20441  dchrelbas3  20477  bcmono  20516  lgsquad2lem2  20598  2sqlem10  20613  pntrsumbnd2  20716  pntpbnd1  20735  pntlem3  20758  isexid2  20992  shsvs  21902  0cnop  22559  0cnfn  22560  cnlnssadj  22660  ssmd1  22891  ssmd2  22892  atexch  22961  mdsymlem4  22986  sumdmdlem  22998  ifeqeqx  23034  xppreima  23211  fmptcof2  23229  pwsiga  23491  subfacp1lem6  23716  erdszelem8  23729  cvmliftlem7  23822  cvmliftlem10  23825  cvmlift2lem12  23845  eupai  23883  eupath2  23904  dedekind  24082  trpredlem1  24230  poseq  24253  axlowdimlem15  24584  axcontlem7  24598  endofsegid  24708  broutsideof2  24745  ordcmp  24886  findreccl  24892  areacirclem2  24925  twsymr  25078  eqfnung2  25118  cbcpcp  25162  prl  25167  oriso  25214  dupre1  25243  fsumprd  25329  multinvb  25423  zerdivemp1  25436  svli2  25484  svs3  25488  efilcp  25552  islimrs3  25581  sigadd  25649  clsmulcv  25682  distmlva  25688  intvconlem1  25703  cmpassoh  25801  prismorcsetlemc  25917  domcatfun  25925  gltpntl  26072  lineval4a  26087  isconcl6ab  26104  xsyysx  26145  bsstrs  26146  nbssntrs  26147  a1i13  26200  a1i24  26203  nn0prpwlem  26238  nn0prpw  26239  sdclem2  26452  fdc  26455  mettrifi  26473  zerdivemp1x  26586  smprngopr  26677  jca3  26710  prtlem80  26724  monotoddzzfi  27027  psgnunilem4  27420  fsumcnf  27692  refsum2cnlem1  27708  stoweidlem29  27778  stoweidlem31  27780  stoweidlem35  27784  reuan  27958  2reu4  27968  funressnfv  27991  ndmaovass  28066  mpt2xopynvov0  28084  nbusgra  28143  nbgra0nb  28144  nbgranself2  28151  nbcusgra  28159  uvtxnbgra  28165  frgra2v  28177  frgra3vlem1  28178  3vfriswmgralem  28182  1to2vfriswmgra  28184  1to3vfriswmgra  28185  ee121  28266  ee122  28267  rspsbc2  28297  a9e2ndeq  28325  vd12  28372  vd13  28373  ee221  28422  ee212  28424  ee112  28427  ee211  28430  ee210  28432  ee201  28434  ee120  28436  ee021  28438  ee012  28440  ee102  28442  ee03  28516  ee31  28527  ee31an  28529  ee123  28538  a9e2ndeqVD  28685  a9e2ndeqALT  28708  bnj151  28909  bnj594  28944  bnj600  28951  ax10lem17ALT  29123  a12lem1  29130  ax9lem17  29156  lfl1dim  29311  lfl1dim2N  29312  lkreqN  29360  cvrexchlem  29608  ps-2  29667  paddasslem14  30022  idldil  30303  isltrn2N  30309  cdleme25a  30542  dibglbN  31356  dihlsscpre  31424  dvh4dimlem  31633  lcfl7N  31691  mapdval2N  31820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator