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 4474 vs. uniexg 4475. (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  1851  equsalh  1852  dvelimfALT  1854  dvelimf-o  1855  equvini  1880  equveli  1881  ax11  1942  ax11v  1991  sbal1  2089  dvelimALT  2097  ax11eq  2108  ax11el  2109  ax11indalem  2113  ax11inda2ALT  2114  ax11inda2  2115  euan  2173  moexex  2185  rgen2a  2582  ralrimivw  2600  reximdv  2627  rexlimdvw  2643  reuind  2934  rexn0  3517  axsep  4100  dtru  4159  fr0  4330  ordsssuc2  4439  reusv6OLD  4503  reusv7OLD  4504  ordsucelsuc  4571  tfinds  4608  tfindsg  4609  limomss  4619  findsg  4641  finds1  4643  poltletr  5052  xpexr  5088  fveqres  5480  fmptco  5611  elunirnALT  5699  ndmovord  5930  soxp  6148  smofvon2  6327  abianfplem  6424  oaordi  6498  oawordeulem  6506  odi  6531  brdomg  6826  map1  6893  fopwdom  6924  fodomr  6966  mapxpen  6981  infensuc  6993  onomeneq  7004  fineqvlem  7031  fineqv  7032  pssnn  7035  xpfi  7082  finsschain  7116  dffi3  7138  fisup2g  7171  fisupcl  7172  inf3lemd  7282  en3lplem2  7371  r1ordg  7404  r1val1  7412  r1pw  7471  r1pwOLD  7472  rankxplim3  7505  carddomi2  7557  fidomtri  7580  pr2ne  7589  alephon  7650  alephcard  7651  alephnbtwn  7652  alephordi  7655  iunfictbso  7695  fin23lem30  7922  fin1a2lem10  7989  domtriomlem  8022  axdc3lem2  8031  axdc3lem4  8033  alephval2  8148  cfpwsdom  8160  axextnd  8167  axrepnd  8170  axpownd  8177  axregnd  8180  axinfndlem1  8181  fpwwe2lem12  8217  wunfi  8297  addnidpi  8479  pinq  8505  ltexprlem7  8620  mulgt0sr  8681  lbinfm  9661  nnind  9718  nn1m1nn  9720  uzindOLD  10059  uzm1  10211  xrltnsym  10424  xrlttri  10426  xrlttr  10427  qbtwnxr  10479  xltnegi  10495  xlt2add  10532  xrsupsslem  10577  xrinfmsslem  10578  xrub  10582  fzospliti  10850  seqfveq2  11020  seqshft2  11024  monoord  11028  seqsplit  11031  seqf1o  11039  seqhomo  11045  faclbnd4lem4  11261  hashf1lem2  11345  hashf1  11346  seqcoll  11352  resqrex  11687  rexuz3  11783  rexanuz2  11784  limsupgre  11906  rlimconst  11969  caurcvg  12100  caucvg  12102  sumss  12148  fsumcl2lem  12155  fsumrlim  12220  fsumo1  12221  nn0seqcvgd  12688  exprmfct  12737  rpexp1i  12748  pcz  12881  pcadd  12885  pcmptcl  12887  prmlem0  13055  ressress  13153  sylow1lem1  14857  efgsf  14986  efgrelexlema  15006  dprdss  15212  dprdsn  15219  ablfac1eulem  15255  lssssr  15658  psrvscafval  16083  mplcoe1  16157  mplcoe2  16159  epttop  16694  cmpsublem  17074  fiuncmp  17079  1stcrest  17127  kgenss  17186  hmeofval  17397  fbun  17483  fgss2  17517  filcon  17526  filuni  17528  filssufilg  17554  filufint  17563  hausflimi  17623  hausflim  17624  hauspwpwf1  17630  fclscmp  17673  alexsubALTlem4  17692  ptcmplem3  17696  ptcmplem5  17698  isxmet2d  17840  imasdsf1olem  17885  blf  17909  metrest  18018  nrginvrcn  18150  nmoge0  18178  nmoleub  18188  fsumcn  18322  cmetcaulem  18662  iscmet3  18667  iscmet2  18668  bcthlem2  18695  ovolicc2lem3  18826  itg2seq  19045  itg2splitlem  19051  itgeq1f  19074  itgeq2  19080  iblcnlem  19091  itgfsum  19129  limcnlp  19176  perfdvf  19201  dvnres  19228  dvmptfsum  19270  c1lip1  19292  mpfrcl  19350  aalioulem5  19664  abelth  19765  sinq12ge0  19824  rlimcnp  20208  xrlimcnp  20211  jensen  20231  ppiublem1  20389  dchrelbas3  20425  bcmono  20464  lgsquad2lem2  20546  2sqlem10  20561  pntrsumbnd2  20664  pntpbnd1  20683  pntlem3  20706  isexid2  20938  shsvs  21848  0cnop  22505  0cnfn  22506  cnlnssadj  22606  ssmd1  22837  ssmd2  22838  atexch  22907  mdsymlem4  22932  sumdmdlem  22944  ifeqeqx  22980  subfacp1lem6  23074  erdszelem8  23087  cvmliftlem7  23180  cvmliftlem10  23183  cvmlift2lem12  23203  eupai  23241  eupath2  23262  dedekind  23439  trpredlem1  23585  poseq  23608  axlowdimlem15  23945  axcontlem7  23959  endofsegid  24069  broutsideof2  24106  ordcmp  24247  findreccl  24253  twsymr  24430  eqfnung2  24471  cbcpcp  24515  prl  24520  oriso  24567  dupre1  24596  fsumprd  24682  multinvb  24776  zerdivemp1  24789  svli2  24837  svs3  24841  efilcp  24905  islimrs3  24934  sigadd  25002  clsmulcv  25035  distmlva  25041  intvconlem1  25056  cmpassoh  25154  prismorcsetlemc  25270  domcatfun  25278  gltpntl  25425  lineval4a  25440  isconcl6ab  25457  xsyysx  25498  bsstrs  25499  nbssntrs  25500  a1i13  25553  a1i24  25556  nn0prpwlem  25591  nn0prpw  25592  sdclem2  25805  fdc  25808  mettrifi  25826  zerdivemp1x  25939  smprngopr  26030  jca3  26063  prtlem80  26077  monotoddzzfi  26380  psgnunilem4  26773  fsumcnf  27046  refsum2cnlem1  27062  stoweidlem29  27099  stoweidlem31  27101  stoweidlem35  27105  ee121  27303  ee122  27304  ra4sbc2  27334  a9e2ndeq  27362  vd12  27406  vd13  27407  ee221  27456  ee212  27458  ee112  27461  ee211  27464  ee210  27466  ee201  27468  ee120  27470  ee021  27472  ee012  27474  ee102  27476  ee03  27550  ee31  27561  ee31an  27563  ee123  27572  a9e2ndeqVD  27719  a9e2ndeqALT  27742  bnj151  27942  bnj594  27977  bnj600  27984  ax12olem16K  28212  ax12olem16X  28213  ax10lem24X  28244  ax10lem17ALT  28274  a12lem1  28281  ax9lem17  28307  lfl1dim  28462  lfl1dim2N  28463  lkreqN  28511  cvrexchlem  28759  ps-2  28818  paddasslem14  29173  idldil  29454  isltrn2N  29460  cdleme25a  29693  dibglbN  30507  dihlsscpre  30575  dvh4dimlem  30784  lcfl7N  30842  mapdval2N  30971
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator