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 4453 vs. uniexg 4454. (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  2580  ralrimivw  2598  reximdv  2625  rexlimdvw  2641  reuind  2917  rexn0  3498  axsep  4080  dtru  4139  fr0  4309  ordsssuc2  4418  reusv6OLD  4482  reusv7OLD  4483  ordsucelsuc  4550  tfinds  4587  tfindsg  4588  limomss  4598  findsg  4620  finds1  4622  poltletr  5031  xpexr  5067  fveqres  5459  fmptco  5590  elunirnALT  5678  ndmovord  5909  soxp  6127  smofvon2  6306  abianfplem  6403  oaordi  6477  oawordeulem  6485  odi  6510  brdomg  6805  map1  6872  fopwdom  6903  fodomr  6945  mapxpen  6960  infensuc  6972  onomeneq  6983  fineqvlem  7010  fineqv  7011  pssnn  7014  xpfi  7061  finsschain  7095  dffi3  7117  fisup2g  7150  fisupcl  7151  inf3lemd  7261  en3lplem2  7350  r1ordg  7383  r1val1  7391  r1pw  7450  r1pwOLD  7451  rankxplim3  7484  carddomi2  7536  fidomtri  7559  pr2ne  7568  alephon  7629  alephcard  7630  alephnbtwn  7631  alephordi  7634  iunfictbso  7674  fin23lem30  7901  fin1a2lem10  7968  domtriomlem  8001  axdc3lem2  8010  axdc3lem4  8012  alephval2  8127  cfpwsdom  8139  axextnd  8146  axrepnd  8149  axpownd  8156  axregnd  8159  axinfndlem1  8160  fpwwe2lem12  8196  wunfi  8276  addnidpi  8458  pinq  8484  ltexprlem7  8599  mulgt0sr  8660  lbinfm  9640  nnind  9697  nn1m1nn  9699  uzindOLD  10038  uzm1  10190  xrltnsym  10403  xrlttri  10405  xrlttr  10406  qbtwnxr  10458  xltnegi  10474  xlt2add  10511  xrsupsslem  10556  xrinfmsslem  10557  xrub  10561  fzospliti  10829  seqfveq2  10999  seqshft2  11003  monoord  11007  seqsplit  11010  seqf1o  11018  seqhomo  11024  faclbnd4lem4  11240  hashf1lem2  11324  hashf1  11325  seqcoll  11331  resqrex  11666  rexuz3  11762  rexanuz2  11763  limsupgre  11885  rlimconst  11948  caurcvg  12079  caucvg  12081  sumss  12127  fsumcl2lem  12134  fsumrlim  12199  fsumo1  12200  nn0seqcvgd  12667  exprmfct  12716  rpexp1i  12727  pcz  12860  pcadd  12864  pcmptcl  12866  prmlem0  13034  ressress  13132  sylow1lem1  14836  efgsf  14965  efgrelexlema  14985  dprdss  15191  dprdsn  15198  ablfac1eulem  15234  lssssr  15637  psrvscafval  16062  mplcoe1  16136  mplcoe2  16138  epttop  16673  cmpsublem  17053  fiuncmp  17058  1stcrest  17106  kgenss  17165  hmeofval  17376  fbun  17462  fgss2  17496  filcon  17505  filuni  17507  filssufilg  17533  filufint  17542  hausflimi  17602  hausflim  17603  hauspwpwf1  17609  fclscmp  17652  alexsubALTlem4  17671  ptcmplem3  17675  ptcmplem5  17677  isxmet2d  17819  imasdsf1olem  17864  blf  17888  metrest  17997  nrginvrcn  18129  nmoge0  18157  nmoleub  18167  fsumcn  18301  cmetcaulem  18641  iscmet3  18646  iscmet2  18647  bcthlem2  18674  ovolicc2lem3  18805  itg2seq  19024  itg2splitlem  19030  itgeq1f  19053  itgeq2  19059  iblcnlem  19070  itgfsum  19108  limcnlp  19155  perfdvf  19180  dvnres  19207  dvmptfsum  19249  c1lip1  19271  mpfrcl  19329  aalioulem5  19643  abelth  19744  sinq12ge0  19803  rlimcnp  20187  xrlimcnp  20190  jensen  20210  ppiublem1  20368  dchrelbas3  20404  bcmono  20443  lgsquad2lem2  20525  2sqlem10  20540  pntrsumbnd2  20643  pntpbnd1  20662  pntlem3  20685  isexid2  20917  shsvs  21827  0cnop  22484  0cnfn  22485  cnlnssadj  22585  ssmd1  22816  ssmd2  22817  atexch  22886  mdsymlem4  22911  sumdmdlem  22923  ifeqeqx  22959  subfacp1lem6  23053  erdszelem8  23066  cvmliftlem7  23159  cvmliftlem10  23162  cvmlift2lem12  23182  eupai  23220  eupath2  23241  dedekind  23418  trpredlem1  23564  poseq  23587  axlowdimlem15  23924  axcontlem7  23938  endofsegid  24048  broutsideof2  24085  ordcmp  24226  findreccl  24232  twsymr  24409  eqfnung2  24450  cbcpcp  24494  prl  24499  oriso  24546  dupre1  24575  fsumprd  24661  multinvb  24755  zerdivemp1  24768  svli2  24816  svs3  24820  efilcp  24884  islimrs3  24913  sigadd  24981  clsmulcv  25014  distmlva  25020  intvconlem1  25035  cmpassoh  25133  prismorcsetlemc  25249  domcatfun  25257  gltpntl  25404  lineval4a  25419  isconcl6ab  25436  xsyysx  25477  bsstrs  25478  nbssntrs  25479  a1i13  25532  a1i24  25535  nn0prpwlem  25570  nn0prpw  25571  sdclem2  25784  fdc  25787  mettrifi  25805  zerdivemp1x  25918  smprngopr  26009  jca3  26042  prtlem80  26056  monotoddzzfi  26359  psgnunilem4  26752  fsumcnf  27025  refsum2cnlem1  27041  stoweidlem29  27078  stoweidlem31  27080  stoweidlem35  27084  ee121  27282  ee122  27283  ra4sbc2  27313  a9e2ndeq  27341  vd12  27385  vd13  27386  ee221  27435  ee212  27437  ee112  27440  ee211  27443  ee210  27445  ee201  27447  ee120  27449  ee021  27451  ee012  27453  ee102  27455  ee03  27529  ee31  27540  ee31an  27542  ee123  27551  a9e2ndeqVD  27698  a9e2ndeqALT  27721  bnj151  27921  bnj594  27956  bnj600  27963  ax12olem16K  28191  ax12olem16X  28192  ax10lem24X  28223  ax10lem17ALT  28253  a12lem1  28260  ax9lem17  28286  lfl1dim  28441  lfl1dim2N  28442  lkreqN  28490  cvrexchlem  28738  ps-2  28797  paddasslem14  29152  idldil  29433  isltrn2N  29439  cdleme25a  29672  dibglbN  30486  dihlsscpre  30554  dvh4dimlem  30763  lcfl7N  30821  mapdval2N  30950
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator