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

Theorem a1d 25
Description: Deduction introducing an embedded antecedent. Deduction form of ax-1 6 and a1i 11. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Hypothesis
Ref Expression
a1d.1 (𝜑𝜓)
Assertion
Ref Expression
a1d (𝜑 → (𝜒𝜓))

Proof of Theorem a1d
StepHypRef Expression
1 a1d.1 . 2 (𝜑𝜓)
2 ax-1 6 . 2 (𝜓 → (𝜒𝜓))
31, 2syl 17 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  2a1d  26  a1i13  27  syl5com  31  mpid  42  syld  45  imim2d  54  syl6ci  68  syl5d  70  syl6d  72  pm2.21d  116  pm2.24d  145  pm2.51  163  pm2.521  164  pm2.61iii  177  mtod  187  impbid21d  199  imbi2d  328  adantr  479  jctild  563  jctird  564  pm3.4  581  anbi2d  735  anbi1d  736  ad4ant13  1283  ad4ant134  1287  ad4ant24  1289  meredith  1556  ax12  2196  ax12OLD  2233  nfsb4t  2281  ax12vALT  2320  moexex  2433  pm2.61da3ne  2775  ralrimivw  2854  reximdv  2903  rexlimdvw  2920  reuind  3282  sbcimdvOLD  3370  rexn0  3929  eqoreldifOLD  4076  tppreqb  4180  prnebg  4228  elpreqprlem  4232  axsep  4606  dtru  4682  fr0  4911  ssrel2  5026  poltletr  5338  ordsssuc2  5618  ndmfv  6011  fveqres  6023  fmptco  6186  tpres  6247  fntpb  6254  elunirn  6289  isof1oopb  6351  ndmovord  6597  ordsucelsuc  6789  tfinds  6826  tfindsg  6827  limomss  6837  findsg  6860  finds1  6862  xpexr  6873  bropopvvv  7016  bropfvvvvlem  7017  bropfvvvv  7018  soxp  7051  suppun  7076  extmptsuppeq  7080  funsssuppss  7082  suppss  7086  suppssov1  7088  suppss2  7090  suppssfv  7092  mpt2xopynvov0  7105  smofvon2  7215  oaordi  7388  oawordeulem  7396  odi  7421  brdomg  7726  map1  7796  fopwdom  7828  fodomr  7871  mapxpen  7886  infensuc  7898  onomeneq  7910  fineqvlem  7934  fineqv  7935  xpfi  7991  finsschain  8031  fsuppun  8052  fsuppunbi  8054  funsnfsupp  8057  dffi3  8095  fisup2g  8132  fisupcl  8133  fiinf2g  8164  wemapso2  8216  en3lplem2  8270  inf3lemd  8282  r1ordg  8399  r1val1  8407  r1pw  8466  r1pwALT  8467  rankxplim3  8502  carddomi2  8554  fidomtri  8577  pr2ne  8586  alephon  8650  alephcard  8651  alephnbtwn  8652  alephordi  8655  iunfictbso  8695  fin23lem30  8922  fin1a2lem10  8989  axdc3lem2  9031  axdc3lem4  9033  alephval2  9148  cfpwsdom  9160  axextnd  9167  axrepnd  9170  axpownd  9177  axregnd  9180  axinfndlem1  9181  fpwwe2lem12  9217  wunfi  9297  addnidpi  9477  pinq  9503  mulgt0sr  9680  dedekind  9950  nnind  10792  nn1m1nn  10794  nn0n0n1ge2b  11113  nn0lt2  11180  uzm1  11457  uzinfi  11507  nn01to3  11522  xrltnsym  11714  xrlttri  11716  xrlttr  11717  qbtwnxr  11773  xltnegi  11789  xlt2add  11828  xrsupsslem  11874  xrinfmsslem  11875  xrub  11879  reltxrnmnf  11911  fzospliti  12236  elfzonlteqm1  12277  elfznelfzo  12306  injresinjlem  12317  injresinj  12318  modfzo0difsn  12471  addmodlteq  12474  ssnn0fi  12513  fsuppmapnn0fiub0  12522  suppssfz  12523  seqfveq2  12552  seqshft2  12556  monoord  12560  seqsplit  12563  seqf1o  12571  seqhomo  12577  faclbnd4lem4  12812  hasheqf1oi  12866  hasheqf1oiOLD  12867  hashrabsn1  12888  hashgt0elex  12913  hash1snb  12931  hashf1lem2  12960  hashf1  12961  seqcoll  12968  pr2pwpr  12977  hashge2el2difr  12979  2swrd1eqwrdeq  13163  swrdswrd  13169  swrdccatin1  13191  swrdccatin12lem3  13198  swrdccat3  13200  swrdccat3blem  13203  repsdf2  13233  repswsymballbi  13235  cshw0  13248  cshwmodn  13249  cshwn  13251  cshwcl  13252  cshwlen  13253  cshw1  13276  2cshwcshw  13279  cshimadifsn  13283  s3sndisj  13411  s3iunsndisj  13412  relexprelg  13483  relexpnndm  13486  relexpaddg  13498  relexpaddd  13499  resqrex  13696  rexuz3  13793  rexanuz2  13794  limsupgre  13922  rlimconst  13987  caurcvg  14121  caurcvgOLD  14122  caucvg  14124  sumss  14169  fsumcl2lem  14176  modfsummods  14233  fsumrlim  14251  fsumo1  14252  fprodcl2lem  14386  dvdsaddre2b  14734  dvdsabseq  14740  zeneo  14768  mod2eq1n2dvds  14776  nno  14803  sumeven  14815  sumodd  14816  nn0seqcvgd  14995  lcmdvds  15033  lcmfunsnlem2  15065  lcmfunsnlem  15066  divgcdcoprm0  15091  exprmfct  15128  rpexp1i  15145  prm23lt5  15239  prm23ge5  15240  pcz  15305  pcadd  15313  pcmptcl  15315  oddprmdvds  15327  prmgaplem5  15479  prmgaplem6  15480  prmgaplem7  15481  cshwshashlem1  15522  cshwsdisj  15525  prmlem0  15532  ressress  15647  initoeu2lem2  16378  mgm2nsgrplem2  17119  mgm2nsgrplem3  17120  dfgrp2e  17161  dfgrp3e  17228  symgextf1  17554  gsmsymgrfix  17561  gsmsymgreq  17565  sylow1lem1  17742  efgsf  17871  efgrelexlema  17891  dprdss  18156  ablfac1eulem  18199  lssssr  18676  01eq0ring  18995  psrvscafval  19113  mplcoe1  19188  mplcoe5  19191  mpfrcl  19241  psgnodpm  19657  mamudm  19914  matmulcell  19971  dmatmul  20023  scmatsgrp1  20048  mavmuldm  20076  mavmulsolcl  20077  mdetunilem9  20146  cramerlem3  20215  cramer0  20216  chpscmatgsumbin  20369  chp0mat  20371  fvmptnn04ifc  20377  fvmptnn04ifd  20378  epttop  20524  neiptopnei  20647  fiuncmp  20918  1stcrest  20967  comppfsc  21046  kgenss  21057  hmeofval  21272  fbun  21355  fgss2  21389  filuni  21400  filssufilg  21426  filufint  21435  hausflimi  21495  hausflim  21496  hauspwpwf1  21502  fclscmp  21545  alexsubALTlem4  21565  ptcmplem3  21569  ptcmplem5  21571  cstucnd  21799  isxmet2d  21842  imasdsf1olem  21888  blfps  21921  blf  21922  metrest  22039  nrginvrcn  22194  nmoge0  22226  nmoleub  22236  nmoge0OLD  22244  nmoleubOLD  22252  fsumcn  22402  cmetcaulem  22759  iscmet3  22764  iscmet2  22765  bcthlem2  22794  ovolicc2lem3  22970  itg2seq  23191  itg2splitlem  23197  itgeq1f  23220  itgeq2  23226  iblcnlem  23237  itgfsum  23275  limcnlp  23324  perfdvf  23349  dvnres  23376  dvmptfsum  23418  c1lip1  23440  abelth  23887  sinq12ge0  23952  rlimcnp  24380  xrlimcnp  24383  jensen  24403  ppiublem1  24617  dchrelbas3  24653  bcmono  24692  zabsle1  24711  gausslemma2dlem0f  24776  gausslemma2dlem1a  24780  gausslemma2dlem4  24784  lgsquad2lem2  24800  2lgslem1a1  24804  2lgslem3  24819  2lgs  24822  2lgsoddprm  24831  2sqlem10  24843  pntrsumbnd2  24946  pntpbnd1  24965  pntlem3  24988  axcontlem7  25541  ausisusgra  25623  usgraidx2v  25661  nbgra0nb  25697  nbgranself2  25704  nbgraf1olem3  25711  nbgraf1olem5  25713  nb3graprlem1  25719  nbcusgra  25731  cusgrasizeinds  25743  usgra2wlkspthlem1  25886  wwlkm1edg  26002  wwlknfi  26005  clwwlkprop  26037  clwwlknprop  26039  clwlkisclwwlklem2a  26052  el2wlkonotot0  26138  usg2wlkonot  26149  usg2wotspth  26150  2spontn0vne  26153  vdgrf  26164  cusgraiffrusgra  26206  rusgraprop4  26210  rusgrasn  26211  eupai  26233  eupath2  26246  frgra2v  26265  frgra3vlem1  26266  3vfriswmgralem  26270  1to2vfriswmgra  26272  1to3vfriswmgra  26273  2pthfrgra  26277  vdfrgra0  26288  vdgn1frgrav2  26292  frgrawopreglem2  26311  frgrawopreglem3  26312  frgrawopreglem4  26313  frgrawopreg  26315  frgraregorufr0  26318  frgraregorufr  26319  2spotdisj  26327  2spotiundisj  26328  2spotmdisj  26334  numclwwlkovf2ex  26352  extwwlkfab  26356  frgrareggt1  26382  frgrareg  26383  frgraregord13  26385  aevdemo  26448  shsvs  27355  0cnop  28011  0cnfn  28012  cnlnssadj  28112  ssmd1  28343  ssmd2  28344  atexch  28413  mdsymlem4  28438  sumdmdlem  28450  ifeqeqx  28534  fmptcof2  28628  padct  28674  nnindf  28748  pwsiga  29317  ldsysgenld  29347  fiunelros  29361  bnj151  30047  bnj594  30082  bnj600  30089  subfacp1lem6  30267  erdszelem8  30280  cvmliftlem7  30373  cvmliftlem10  30376  cvmlift2lem12  30396  mrsubfval  30505  msubfval  30521  mclsssvlem  30559  trpredlem1  30814  poseq  30837  funpartfv  31058  endofsegid  31198  broutsideof2  31235  a1i24  31301  nn0prpwlem  31322  nn0prpw  31323  ordcmp  31451  findreccl  31457  bj-alsb  31649  bj-ax6e  31677  bj-ax12v3ALT  31698  bj-ax12v  31794  bj-axsep  31823  bj-dtru  31827  bj-xpnzex  31971  bj-xnex  32077  finxp00  32247  wl-spae  32359  wl-nfs1t  32378  poimirlem27  32481  ovoliunnfl  32496  voliunnfl  32498  volsupnfl  32499  itg2addnclem3  32508  itg2addnc  32509  ftc1anc  32538  areacirclem1  32545  sdclem2  32583  fdc  32586  mettrifi  32598  isexid2  32699  zerdivemp1x  32791  smprngopr  32896  mpt2bi123f  33016  mptbi12f  33020  ac6s6  33025  jca3  33031  ax12fromc15  33083  hbequid  33087  dvelimf-o  33107  ax12eq  33119  ax12el  33120  ax12indalem  33123  ax12inda2ALT  33124  ax12inda2  33125  lfl1dim  33301  lfl1dim2N  33302  lkreqN  33350  cvrexchlem  33598  ps-2  33657  paddasslem14  34012  idldil  34293  isltrn2N  34299  cdleme25a  34534  dibglbN  35348  dihlsscpre  35416  dvh4dimlem  35625  lcfl7N  35683  mapdval2N  35812  monotoddzzfi  36400  rp-fakeimass  36758  clublem  36818  relexpnul  36871  ee121  37614  ee122  37615  rspsbc2  37647  ax6e2ndeq  37678  vd12  37728  vd13  37729  ee221  37778  ee212  37780  ee112  37783  ee211  37786  ee210  37788  ee201  37790  ee120  37792  ee021  37794  ee012  37796  ee102  37798  ee03  37871  ee31  37882  ee31an  37884  ee123  37893  ax6e2ndeqVD  38049  ax6e2ndeqALT  38071  refsum2cnlem1  38101  fiiuncl  38142  eliin2f  38199  disjrnmpt2  38254  disjinfi  38259  allbutfi  38443  mccl  38551  constlimc  38577  limclner  38605  ioodvbdlimc1lem2  38709  ioodvbdlimc1lem2OLD  38711  ioodvbdlimc2lem  38713  ioodvbdlimc2lemOLD  38714  dvmptfprod  38725  dvnprodlem3  38728  stoweidlem31  38814  pwsal  39105  prsal  39108  sge0pnffigt  39183  sge0ltfirp  39187  0ome  39313  hoicvrrex  39340  hoidmvle  39384  ovnhoilem1  39385  ovnlecvr2  39394  smflimlem3  39553  reuan  39723  2reu4  39733  funressnfv  39751  ndmaovass  39830  nltle2tri  39837  smonoord  39839  iccpartigtl  39856  icceuelpartlem  39868  iccpartnel  39871  fmtnoprmfac1  39910  fmtnoprmfac2  39912  prmdvdsfmtnof1lem2  39930  31prm  39945  lighneallem3  39957  lighneallem4b  39959  lighneallem4  39960  lighneal  39961  nn0o1gt2ALTV  40038  nn0oALTV  40040  stgoldbwt  40093  bgoldbwt  40094  sgoldbalt  40098  nnsum3primesgbe  40103  wtgoldbnnsum4prm  40113  bgoldbnnsum3prm  40115  bgoldbtbndlem2  40117  bgoldbtbndlem3  40118  bgoldbtbndlem4  40119  bgoldbtbnd  40120  bgoldbachlt  40122  tgblthelfgott  40124  bgoldbachltOLD  40129  tgblthelfgottOLD  40131  pfxccat3  40184  n0snor2el  40213  propeqop  40216  propssopi  40217  ssprsseq  40219  otiunsndisjX  40222  funsndifnop  40238  fundmge2nop0  40242  fzoopth  40277  xnn0xaddcl  40305  ausgrusgrb  40487  usgredg2v  40546  lfuhgr1v0e  40572  subumgredg2  40601  fusgrfisbase  40639  nbuhgr  40657  uhgrnbgr0nb  40668  nbgr0vtxlem  40669  nbgr1vtx  40672  uvtxa0  40712  uvtx2vtx1edg  40717  cusgredg  40738  cusgrsizeinds  40760  sizusglecusg  40771  ewlkle  40899  upgr1wlkwlk  40939  pthdivtx  41027  usgr2trlncl  41058  cyclnsPth  41098  crctcsh1wlkn0lem4  41108  wwlksn  41132  iswwlksnon  41143  iswspthsnon  41144  wwlksm1edg  41170  wwlksnfi  41204  wwlksnonfi  41219  wspn0  41223  2pthdlem1  41229  umgr2wlk  41248  2wspdisj  41257  2wspiundisj  41258  clwwlksn  41281  clwlkclwwlklem2a  41299  clwlkclwwlk  41303  umgrclwwlksge2  41311  clwwlksnfi  41312  clwwisshclwws  41327  clwwnisshclwwsn  41329  3pthdlem1  41423  eupth2  41499  nfrgr2v  41534  frgr3vlem1  41535  1to2vfriswmgr  41541  1to3vfriswmgr  41542  vdgn1frgrv2  41558  frgrwopreglem3  41575  frgrwopreglem4  41576  frgrwopreg  41578  frgrregorufr0  41581  frgrregorufr  41582  fusgr2wsp2nb  41590  2wspmdisj  41593  av-numclwwlkovf2ex  41609  av-extwwlkfab  41612  av-frgrareggt1  41639  av-frgrareg  41640  av-frgraregord13  41642  nrhmzr  41755  rngccatidALTV  41873  funcrngcsetcALT  41883  ringccatidALTV  41936  nn0le2is012  42030  lincdifsn  42099  lindslinindimp2lem1  42133  lindsrng01  42143  ldepsnlinc  42183  m1modmmod  42202  blen1b  42272  nn0sumshdiglemB  42304  nn0sumshdiglem1  42305
  Copyright terms: Public domain W3C validator