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  meredith  1556  ax12  2290  ax12OLD  2327  nfsb4t  2375  ax12vALT  2414  moexex  2527  pm2.61da3ne  2869  ralrimivw  2948  reximdv  2997  rexlimdvw  3014  reuind  3376  sbcimdvOLD  3464  rexn0  4024  eqoreldifOLD  4171  tppreqb  4275  prnebg  4323  elpreqprlem  4327  axsep  4701  dtru  4777  fr0  5006  ssrel2  5121  poltletr  5433  ordsssuc2  5716  ordnbtwn  5718  ndmfv  6112  fveqres  6124  fmptco  6287  tpres  6348  fntpb  6355  elunirn  6390  isof1oopb  6452  ndmovord  6698  ordsucelsuc  6890  tfinds  6927  tfindsg  6928  limomss  6938  findsg  6961  finds1  6963  xpexr  6975  bropopvvv  7118  bropfvvvvlem  7119  bropfvvvv  7120  soxp  7153  suppun  7178  extmptsuppeq  7182  funsssuppss  7184  suppss  7188  suppssov1  7190  suppss2  7192  suppssfv  7194  mpt2xopynvov0  7207  smofvon2  7316  oaordi  7489  oawordeulem  7497  odi  7522  brdomg  7827  map1  7897  fopwdom  7929  fodomr  7972  mapxpen  7987  infensuc  7999  onomeneq  8011  fineqvlem  8035  fineqv  8036  xpfi  8092  finsschain  8132  fsuppun  8153  fsuppunbi  8155  funsnfsupp  8158  dffi3  8196  fisup2g  8233  fisupcl  8234  fiinf2g  8265  wemapso2  8317  en3lplem2  8371  inf3lemd  8383  r1ordg  8500  r1val1  8508  r1pw  8567  r1pwALT  8568  rankxplim3  8603  carddomi2  8655  fidomtri  8678  pr2ne  8687  alephon  8751  alephcard  8752  alephnbtwn  8753  alephordi  8756  iunfictbso  8796  fin23lem30  9023  fin1a2lem10  9090  axdc3lem2  9132  axdc3lem4  9134  alephval2  9249  cfpwsdom  9261  axextnd  9268  axrepnd  9271  axpownd  9278  axregnd  9281  axinfndlem1  9282  fpwwe2lem12  9318  wunfi  9398  addnidpi  9578  pinq  9604  mulgt0sr  9781  dedekind  10050  nnind  10884  nn1m1nn  10886  nn0n0n1ge2b  11205  nn0lt2  11272  uzm1  11549  uzinfi  11599  nn01to3  11612  xrltnsym  11804  xrlttri  11806  xrlttr  11807  qbtwnxr  11863  xltnegi  11879  xlt2add  11918  xrsupsslem  11964  xrinfmsslem  11965  xrub  11969  reltxrnmnf  11998  fzospliti  12323  elfzonlteqm1  12364  elfznelfzo  12393  injresinjlem  12404  injresinj  12405  modfzo0difsn  12558  addmodlteq  12561  ssnn0fi  12600  fsuppmapnn0fiub0  12609  suppssfz  12610  seqfveq2  12639  seqshft2  12643  monoord  12647  seqsplit  12650  seqf1o  12658  seqhomo  12664  faclbnd4lem4  12899  hasheqf1oi  12953  hasheqf1oiOLD  12954  hashrabsn1  12975  hashgt0elex  13001  hash1snb  13019  hashf1lem2  13048  hashf1  13049  seqcoll  13056  pr2pwpr  13065  hashge2el2difr  13067  2swrd1eqwrdeq  13251  swrdswrd  13257  swrdccatin1  13279  swrdccatin12lem3  13286  swrdccat3  13288  swrdccat3blem  13291  repsdf2  13321  repswsymballbi  13323  cshw0  13336  cshwmodn  13337  cshwn  13339  cshwcl  13340  cshwlen  13341  cshw1  13364  2cshwcshw  13367  cshimadifsn  13371  s3sndisj  13499  s3iunsndisj  13500  relexprelg  13571  relexpnndm  13574  relexpaddg  13586  relexpaddd  13587  resqrex  13784  rexuz3  13881  rexanuz2  13882  limsupgre  14005  rlimconst  14068  caurcvg  14200  caucvg  14202  sumss  14247  fsumcl2lem  14254  modfsummods  14311  fsumrlim  14329  fsumo1  14330  fprodcl2lem  14464  dvdsaddre2b  14812  dvdsabseq  14818  zeneo  14846  mod2eq1n2dvds  14854  nno  14881  sumeven  14893  sumodd  14894  nn0seqcvgd  15066  lcmdvds  15104  lcmfunsnlem2  15136  lcmfunsnlem  15137  divgcdcoprm0  15162  exprmfct  15199  rpexp1i  15216  prm23lt5  15302  prm23ge5  15303  pcz  15368  pcadd  15376  pcmptcl  15378  oddprmdvds  15390  prmgaplem5  15542  prmgaplem6  15543  prmgaplem7  15544  cshwshashlem1  15585  cshwsdisj  15588  prmlem0  15595  ressress  15710  initoeu2lem2  16433  mgm2nsgrplem2  17174  mgm2nsgrplem3  17175  dfgrp2e  17216  dfgrp3e  17283  symgextf1  17609  gsmsymgrfix  17616  gsmsymgreq  17620  sylow1lem1  17781  efgsf  17910  efgrelexlema  17930  dprdss  18196  ablfac1eulem  18239  lssssr  18719  01eq0ring  19038  psrvscafval  19156  mplcoe1  19231  mplcoe5  19234  mpfrcl  19284  psgnodpm  19697  mamudm  19954  matmulcell  20011  dmatmul  20063  scmatsgrp1  20088  mavmuldm  20116  mavmulsolcl  20117  mdetunilem9  20186  cramerlem3  20255  cramer0  20256  chpscmatgsumbin  20409  chp0mat  20411  fvmptnn04ifc  20417  fvmptnn04ifd  20418  epttop  20564  neiptopnei  20687  fiuncmp  20958  1stcrest  21007  comppfsc  21086  kgenss  21097  hmeofval  21312  fbun  21395  fgss2  21429  filuni  21440  filssufilg  21466  filufint  21475  hausflimi  21535  hausflim  21536  hauspwpwf1  21542  fclscmp  21585  alexsubALTlem4  21605  ptcmplem3  21609  ptcmplem5  21611  cstucnd  21839  isxmet2d  21882  imasdsf1olem  21928  blfps  21961  blf  21962  metrest  22079  nrginvrcn  22238  nmoge0  22266  nmoleub  22276  fsumcn  22411  cmetcaulem  22811  iscmet3  22816  iscmet2  22817  bcthlem2  22846  ovolicc2lem3  23010  itg2seq  23231  itg2splitlem  23237  itgeq1f  23260  itgeq2  23266  iblcnlem  23277  itgfsum  23315  limcnlp  23364  perfdvf  23389  dvnres  23416  dvmptfsum  23458  c1lip1  23480  abelth  23915  sinq12ge0  23980  rlimcnp  24408  xrlimcnp  24411  jensen  24431  ppiublem1  24643  dchrelbas3  24679  bcmono  24718  zabsle1  24737  gausslemma2dlem0f  24802  gausslemma2dlem1a  24806  gausslemma2dlem4  24810  lgsquad2lem2  24826  2lgslem1a1  24830  2lgslem3  24845  2lgs  24848  2lgsoddprm  24857  2sqlem10  24869  pntrsumbnd2  24972  pntpbnd1  24991  pntlem3  25014  axcontlem7  25567  ausisusgra  25649  usgraidx2v  25687  nbgra0nb  25723  nbgranself2  25730  nbgraf1olem3  25737  nbgraf1olem5  25739  nb3graprlem1  25745  nbcusgra  25757  cusgrasizeinds  25769  usgra2wlkspthlem1  25912  wwlkm1edg  26028  wwlknfi  26031  clwwlkprop  26063  clwwlknprop  26065  clwlkisclwwlklem2a  26078  el2wlkonotot0  26164  usg2wlkonot  26175  usg2wotspth  26176  2spontn0vne  26179  vdgrf  26190  cusgraiffrusgra  26232  rusgraprop4  26236  rusgrasn  26237  eupai  26259  eupath2  26272  frgra2v  26291  frgra3vlem1  26292  3vfriswmgralem  26296  1to2vfriswmgra  26298  1to3vfriswmgra  26299  2pthfrgra  26303  vdfrgra0  26314  vdgn1frgrav2  26318  frgrawopreglem2  26337  frgrawopreglem3  26338  frgrawopreglem4  26339  frgrawopreg  26341  frgraregorufr0  26344  frgraregorufr  26345  2spotdisj  26353  2spotiundisj  26354  2spotmdisj  26360  numclwwlkovf2ex  26378  extwwlkfab  26382  frgrareggt1  26408  frgrareg  26409  frgraregord13  26411  aevdemo  26474  shsvs  27371  0cnop  28027  0cnfn  28028  cnlnssadj  28128  ssmd1  28359  ssmd2  28360  atexch  28429  mdsymlem4  28454  sumdmdlem  28466  ifeqeqx  28550  fmptcof2  28644  padct  28690  nnindf  28757  pwsiga  29325  ldsysgenld  29355  fiunelros  29369  bnj151  30006  bnj594  30041  bnj600  30048  subfacp1lem6  30226  erdszelem8  30239  cvmliftlem7  30332  cvmliftlem10  30335  cvmlift2lem12  30355  mrsubfval  30464  msubfval  30480  mclsssvlem  30518  trpredlem1  30776  poseq  30799  funpartfv  31027  endofsegid  31167  broutsideof2  31204  a1i24  31270  nn0prpwlem  31292  nn0prpw  31293  ordcmp  31421  findreccl  31427  bj-alsb  31619  bj-ax6e  31647  bj-ax12v3ALT  31668  bj-ax12v  31764  bj-axsep  31793  bj-dtru  31797  bj-xpnzex  31941  bj-xnex  32047  finxp00  32217  wl-spae  32287  wl-nfs1t  32305  poimirlem27  32408  ovoliunnfl  32423  voliunnfl  32425  volsupnfl  32426  itg2addnclem3  32435  itg2addnc  32436  ftc1anc  32465  areacirclem1  32472  sdclem2  32510  fdc  32513  mettrifi  32525  isexid2  32626  zerdivemp1x  32718  smprngopr  32823  mpt2bi123f  32943  mptbi12f  32947  ac6s6  32952  jca3  32958  ax12fromc15  33010  hbequid  33014  dvelimf-o  33034  ax12eq  33046  ax12el  33047  ax12indalem  33050  ax12inda2ALT  33051  ax12inda2  33052  lfl1dim  33228  lfl1dim2N  33229  lkreqN  33277  cvrexchlem  33525  ps-2  33584  paddasslem14  33939  idldil  34220  isltrn2N  34226  cdleme25a  34461  dibglbN  35275  dihlsscpre  35343  dvh4dimlem  35552  lcfl7N  35610  mapdval2N  35739  monotoddzzfi  36327  rp-fakeimass  36678  clublem  36738  relexpnul  36791  ee121  37534  ee122  37535  rspsbc2  37567  ax6e2ndeq  37598  vd12  37648  vd13  37649  ee221  37698  ee212  37700  ee112  37703  ee211  37706  ee210  37708  ee201  37710  ee120  37712  ee021  37714  ee012  37716  ee102  37718  ee03  37791  ee31  37802  ee31an  37804  ee123  37813  ax6e2ndeqVD  37969  ax6e2ndeqALT  37991  refsum2cnlem1  38021  fiiuncl  38061  eliin2f  38118  disjrnmpt2  38172  disjinfi  38177  allbutfi  38360  mccl  38468  constlimc  38494  limclner  38521  ioodvbdlimc1lem2  38625  ioodvbdlimc2lem  38627  dvmptfprod  38638  dvnprodlem3  38641  stoweidlem31  38727  pwsal  39014  prsal  39017  sge0pnffigt  39092  sge0ltfirp  39096  0ome  39222  hoicvrrex  39249  hoidmvle  39293  ovnhoilem1  39294  ovnlecvr2  39303  smflimlem3  39462  reuan  39632  2reu4  39642  funressnfv  39660  ndmaovass  39739  nltle2tri  39746  smonoord  39748  iccpartigtl  39765  icceuelpartlem  39777  iccpartnel  39780  fmtnoprmfac1  39819  fmtnoprmfac2  39821  prmdvdsfmtnof1lem2  39839  31prm  39854  lighneallem3  39866  lighneallem4b  39868  lighneallem4  39869  lighneal  39870  nn0o1gt2ALTV  39947  nn0oALTV  39949  stgoldbwt  40002  bgoldbwt  40003  sgoldbalt  40007  nnsum3primesgbe  40012  wtgoldbnnsum4prm  40022  bgoldbnnsum3prm  40024  bgoldbtbndlem2  40026  bgoldbtbndlem3  40027  bgoldbtbndlem4  40028  bgoldbtbnd  40029  bgoldbachlt  40031  tgblthelfgott  40033  bgoldbachltOLD  40038  tgblthelfgottOLD  40040  pfxccat3  40093  n0snor2el  40122  propeqop  40125  propssopi  40126  ssprsseq  40128  otiunsndisjX  40131  funsndifnop  40147  fundmge2nop0  40151  fzoopth  40186  xnn0xaddcl  40214  ausgrusgrb  40396  usgredg2v  40455  lfuhgr1v0e  40481  subumgredg2  40510  fusgrfisbase  40548  nbuhgr  40566  uhgrnbgr0nb  40577  nbgr0vtxlem  40578  nbgr1vtx  40581  uvtxa0  40621  uvtx2vtx1edg  40626  cusgredg  40647  cusgrsizeinds  40669  sizusglecusg  40680  ewlkle  40808  upgr1wlkwlk  40848  pthdivtx  40936  usgr2trlncl  40967  cyclnsPth  41007  crctcsh1wlkn0lem4  41017  wwlksn  41041  iswwlksnon  41052  iswspthsnon  41053  wwlksm1edg  41079  wwlksnfi  41113  wwlksnonfi  41128  wspn0  41132  2pthdlem1  41138  umgr2wlk  41157  2wspdisj  41166  2wspiundisj  41167  clwwlksn  41190  clwlkclwwlklem2a  41208  clwlkclwwlk  41212  umgrclwwlksge2  41220  clwwlksnfi  41221  clwwisshclwws  41236  clwwnisshclwwsn  41238  3pthdlem1  41332  eupth2  41408  nfrgr2v  41443  frgr3vlem1  41444  1to2vfriswmgr  41450  1to3vfriswmgr  41451  vdgn1frgrv2  41467  frgrwopreglem3  41484  frgrwopreglem4  41485  frgrwopreg  41487  frgrregorufr0  41490  frgrregorufr  41491  fusgr2wsp2nb  41499  2wspmdisj  41502  av-numclwwlkovf2ex  41518  av-extwwlkfab  41521  av-frgrareggt1  41548  av-frgrareg  41549  av-frgraregord13  41551  nrhmzr  41664  rngccatidALTV  41782  funcrngcsetcALT  41792  ringccatidALTV  41845  nn0le2is012  41939  lincdifsn  42008  lindslinindimp2lem1  42042  lindsrng01  42052  ldepsnlinc  42092  m1modmmod  42111  blen1b  42181  nn0sumshdiglemB  42213  nn0sumshdiglem1  42214
  Copyright terms: Public domain W3C validator