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  44  syld  47  imim2d  57  syl6ci  71  syl5d  73  syl6d  75  pm2.21d  118  pm2.24d  147  pm2.51  165  pm2.521  166  pm2.61iii  179  mtod  189  impbid21d  201  imbi2d  329  adantr  472  jctild  567  jctird  568  pm3.4  585  anbi2d  742  anbi1d  743  ad4ant134OLD  1163  ad4ant13OLD  1184  meredith  1703  ax12  2437  ax12OLD  2469  nfsb4t  2514  ax12vALT  2553  moexex  2667  pm2.61da3ne  3009  ralrimivw  3093  reximdv  3142  rexlimdvw  3160  reuind  3540  sbcimdvOLD  3628  rexn0  4206  eqoreldifOLD  4358  tppreqb  4469  ssprsseq  4490  n0snor2el  4497  prnebg  4521  prel12g  4532  elpreqprlem  4534  3elpr2eq  4575  disjord  4781  disjiund  4783  axsep  4920  dtru  4994  propssopi  5107  opthhausdorff  5115  fr0  5233  ssrel2  5355  poltletr  5674  ordsssuc2  5963  ordnbtwn  5965  ndmfv  6367  fveqres  6379  fmptco  6547  funsndifnop  6567  tpres  6618  fntpb  6625  elunirn  6660  isof1oopb  6726  fvmptopab  6850  ndmovord  6977  ordsucelsuc  7175  tfinds  7212  tfindsg  7213  limomss  7223  findsg  7246  finds1  7248  xpexr  7259  bropopvvv  7411  bropfvvvvlem  7412  bropfvvvv  7413  soxp  7446  suppun  7471  extmptsuppeq  7475  funsssuppss  7478  suppss  7482  suppssov1  7484  suppss2  7486  suppssfv  7488  mpt2xopynvov0  7501  smofvon2  7610  oaordi  7783  oawordeulem  7791  odi  7816  brdomg  8119  map1  8189  fopwdom  8221  fodomr  8264  mapxpen  8279  infensuc  8291  onomeneq  8303  fineqvlem  8327  fineqv  8328  xpfi  8384  finsschain  8426  fsuppun  8447  fsuppunbi  8449  funsnfsupp  8452  dffi3  8490  fisup2g  8527  fisupcl  8528  fiinf2g  8559  wemapso2  8611  epnsym  8665  en3lplem2  8669  preleqg  8671  inf3lemd  8685  r1ordg  8802  r1val1  8810  r1pw  8869  r1pwALT  8870  rankxplim3  8905  carddomi2  8957  fidomtri  8980  pr2ne  8989  alephon  9053  alephcard  9054  alephnbtwn  9055  alephordi  9058  iunfictbso  9098  fin23lem30  9327  fin1a2lem10  9394  axdc3lem2  9436  axdc3lem4  9438  alephval2  9557  cfpwsdom  9569  axextnd  9576  axrepnd  9579  axpownd  9586  axregnd  9589  axinfndlem1  9590  fpwwe2lem12  9626  wunfi  9706  addnidpi  9886  pinq  9912  mulgt0sr  10089  dedekind  10363  nnind  11201  nn1m1nn  11203  nn0n0n1ge2b  11522  nn0lt2  11603  nn0le2is012  11604  uzm1  11882  uzinfi  11932  nn01to3  11945  xrltnsym  12134  xrlttri  12136  xrlttr  12137  qbtwnxr  12195  xltnegi  12211  xnn0xaddcl  12230  xlt2add  12254  xrsupsslem  12301  xrinfmsslem  12302  xrub  12306  reltxrnmnf  12336  fzospliti  12665  elfzonlteqm1  12709  elfznelfzo  12738  injresinjlem  12753  injresinj  12754  modfzo0difsn  12907  addmodlteq  12910  ssnn0fi  12949  fsuppmapnn0fiub0  12958  suppssfz  12959  seqfveq2  12988  monoord  12996  seqf1o  13007  seqhomo  13013  faclbnd4lem4  13248  hasheqf1oi  13305  hashrabsn1  13326  hashgt0elex  13352  hash1snb  13370  hashf1lem2  13403  hashf1  13404  seqcoll  13411  hashle2pr  13422  pr2pwpr  13424  hashge2el2difr  13426  2swrd1eqwrdeq  13625  swrdswrd  13631  swrdccatin1  13654  swrdccatin12lem3  13661  swrdccat3  13663  swrdccat3blem  13666  repsdf2  13696  repswsymballbi  13698  cshw0  13711  cshwmodn  13712  cshwn  13714  cshwcl  13715  cshwlen  13716  cshw1  13739  2cshwcshw  13742  cshimadifsn  13746  s3sndisj  13878  s3iunsndisj  13879  relexprelg  13948  relexpnndm  13951  relexpaddg  13963  relexpaddd  13964  resqrex  14161  rexuz3  14258  rexanuz2  14259  limsupgre  14382  rlimconst  14445  caurcvg  14577  caucvg  14579  sumss  14625  fsumcl2lem  14632  modfsummods  14695  fsumrlim  14713  fsumo1  14714  fprodcl2lem  14850  dvdsaddre2b  15202  dvdsabseq  15208  mod2eq1n2dvds  15244  nno  15271  sumeven  15283  sumodd  15284  nn0seqcvgd  15456  lcmdvds  15494  lcmfunsnlem2  15526  lcmfunsnlem  15527  divgcdcoprm0  15552  exprmfct  15589  rpexp1i  15606  prm23lt5  15692  prm23ge5  15693  pcz  15758  pcadd  15766  pcmptcl  15768  oddprmdvds  15780  prmgaplem5  15932  prmgaplem6  15933  prmgaplem7  15934  cshwshashlem1  15975  cshwsdisj  15978  prmlem0  15985  setsstruct  16071  ressress  16111  initoeu2lem2  16837  mgm2nsgrplem2  17578  mgm2nsgrplem3  17579  dfgrp2e  17620  dfgrp3e  17687  symgextf1  18012  gsmsymgrfix  18019  gsmsymgreq  18023  sylow1lem1  18184  efgsf  18313  efgrelexlema  18333  dprdss  18599  ablfac1eulem  18642  lssssr  19126  01eq0ring  19445  psrvscafval  19563  mplcoe1  19638  mplcoe5  19641  mpfrcl  19691  psgnodpm  20107  mamudm  20367  matmulcell  20424  dmatmul  20476  scmatsgrp1  20501  mavmuldm  20529  mavmulsolcl  20530  mdetunilem9  20599  cramerlem3  20668  cramer0  20669  chpscmatgsumbin  20822  chp0mat  20824  fvmptnn04ifc  20830  fvmptnn04ifd  20831  epttop  20986  neiptopnei  21109  fiuncmp  21380  1stcrest  21429  comppfsc  21508  kgenss  21519  hmeofval  21734  fbun  21816  fgss2  21850  filuni  21861  filssufilg  21887  filufint  21896  hausflimi  21956  hausflim  21957  hauspwpwf1  21963  fclscmp  22006  alexsubALTlem4  22026  ptcmplem3  22030  ptcmplem5  22032  cstucnd  22260  isxmet2d  22304  imasdsf1olem  22350  blfps  22383  blf  22384  metrest  22501  nrginvrcn  22668  nmoge0  22697  nmoleub  22707  fsumcn  22845  cmetcaulem  23257  iscmet3  23262  iscmet2  23263  bcthlem2  23293  ovolicc2lem3  23458  itg2seq  23679  itg2splitlem  23685  itgeq1f  23708  itgeq2  23714  iblcnlem  23725  itgfsum  23763  limcnlp  23812  perfdvf  23837  dvnres  23864  dvmptfsum  23908  c1lip1  23930  abelth  24365  sinq12ge0  24430  rlimcnp  24862  xrlimcnp  24865  jensen  24885  ppiublem1  25097  dchrelbas3  25133  bcmono  25172  zabsle1  25191  gausslemma2dlem0f  25256  gausslemma2dlem1a  25260  gausslemma2dlem4  25264  lgsquad2lem2  25280  2lgslem1a1  25284  2lgslem3  25299  2lgs  25302  2lgsoddprm  25311  2sqlem10  25323  pntrsumbnd2  25426  pntpbnd1  25445  pntlem3  25468  axcontlem7  26020  ausgrusgrb  26230  usgredg2v  26289  lfuhgr1v0e  26316  subumgredg2  26347  upgrreslem  26366  umgrreslem  26367  fusgrfisbase  26390  nbuhgr  26409  uhgrnbgr0nb  26420  nbgr0vtxlem  26421  nbgr1vtx  26424  cusgredg  26501  cusgrsizeinds  26529  sizusglecusg  26540  finsumvtxdg2size  26627  ewlkle  26682  upgriswlk  26718  pthdivtx  26806  usgr2trlncl  26837  crctcshwlkn0lem4  26887  wwlksn  26911  iswwlksnon  26928  iswwlksnonOLD  26929  iswspthsnon  26932  iswspthsnonOLD  26933  wwlksm1edg  26961  wwlksnfi  26995  2pthdlem1  27021  umgr2wlk  27040  umgrclwwlkge2  27085  clwlkclwwlklem2a  27092  clwlkclwwlk  27096  clwlkclwwlkf1lem2  27099  clwlkclwwlkf  27102  clwwisshclwws  27109  clwwlknOLD  27123  clwwlknlbonbgr1  27139  clwwlknfi  27145  wwlksext2clwwlk  27158  clwwlknon0  27211  clwwlknonel  27213  clwwlknonwwlknonbOLD  27226  clwwlknonex2e  27230  3pthdlem1  27287  eupth2  27362  nfrgr2v  27397  frgr3vlem1  27398  1to2vfriswmgr  27404  1to3vfriswmgr  27405  vdgn1frgrv2  27421  frgrncvvdeqlem9  27432  frgrwopreglem4a  27435  frgrregorufr0  27449  frgrregorufr  27450  2wspmdisj  27462  2clwwlk2clwwlklem  27474  frgrreggt1  27532  frgrreg  27533  frgrregord13  27535  aevdemo  27599  shsvs  28462  0cnop  29118  0cnfn  29119  cnlnssadj  29219  ssmd1  29450  ssmd2  29451  atexch  29520  mdsymlem4  29545  sumdmdlem  29557  rabeqsnd  29620  ifeqeqx  29639  fmptcof2  29737  padct  29777  nnindf  29845  pwsiga  30473  ldsysgenld  30503  fiunelros  30517  breprexp  30991  bnj151  31225  bnj594  31260  bnj600  31267  subfacp1lem6  31445  erdszelem8  31458  cvmliftlem7  31551  cvmliftlem10  31554  cvmlift2lem12  31574  mrsubfval  31683  msubfval  31699  mclsssvlem  31737  trpredlem1  32003  poseq  32030  nolesgn2o  32101  funpartfv  32329  endofsegid  32469  broutsideof2  32506  a1i24  32572  nn0prpwlem  32594  nn0prpw  32595  ordcmp  32723  findreccl  32729  bj-alsb  32902  bj-ax6e  32930  bj-ax12v3ALT  32953  bj-axsep  33070  bj-dtru  33074  bj-xpnzex  33223  finxp00  33521  wl-spae  33588  wl-nfs1t  33606  poimirlem27  33718  ovoliunnfl  33733  voliunnfl  33735  volsupnfl  33736  itg2addnclem3  33745  itg2addnc  33746  ftc1anc  33775  areacirclem1  33782  sdclem2  33820  fdc  33823  mettrifi  33835  isexid2  33936  zerdivemp1x  34028  smprngopr  34133  mpt2bi123f  34253  mptbi12f  34257  ac6s6  34262  relcnveq3  34385  elrelscnveq3  34533  jca3  34613  ax12fromc15  34663  hbequid  34667  dvelimf-o  34687  ax12eq  34699  ax12el  34700  ax12indalem  34703  ax12inda2ALT  34704  ax12inda2  34705  lfl1dim  34880  lfl1dim2N  34881  lkreqN  34929  cvrexchlem  35177  ps-2  35236  paddasslem14  35591  idldil  35872  isltrn2N  35878  cdleme25a  36112  dibglbN  36926  dihlsscpre  36994  dvh4dimlem  37203  lcfl7N  37261  mapdval2N  37390  monotoddzzfi  37978  rp-fakeimass  38328  clublem  38388  relexpnul  38441  ee121  39182  ee122  39183  rspsbc2  39215  ax6e2ndeq  39246  vd12  39296  vd13  39297  ee221  39346  ee212  39348  ee112  39351  ee211  39354  ee210  39356  ee201  39358  ee120  39360  ee021  39362  ee012  39364  ee102  39366  ee03  39439  ee31  39450  ee31an  39452  ee123  39461  ax6e2ndeqVD  39613  ax6e2ndeqALT  39635  refsum2cnlem1  39664  fiiuncl  39702  eliin2f  39755  disjrnmpt2  39843  disjinfi  39848  rnmptbd2lem  39931  rnmptbdlem  39938  allbutfi  40083  infxrunb3rnmpt  40122  infrpgernmpt  40162  monoordxrv  40179  mccl  40302  constlimc  40328  limclner  40355  xlimmnfvlem1  40530  xlimpnfvlem1  40534  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  dvmptfprod  40632  dvnprodlem3  40635  stoweidlem31  40720  pwsal  41007  prsal  41010  sge0pnffigt  41085  sge0ltfirp  41089  0ome  41218  hoicvrrex  41245  hoidmvle  41289  ovnhoilem1  41290  ovnlecvr2  41299  smflimlem3  41456  reuan  41655  2reu4  41665  funressnfv  41683  ndmaovass  41761  otiunsndisjX  41775  nltle2tri  41802  fzoopth  41816  smonoord  41820  iccpartigtl  41838  icceuelpartlem  41850  iccpartnel  41853  pfxccat3  41905  fmtnoprmfac1  41956  fmtnoprmfac2  41958  prmdvdsfmtnof1lem2  41976  31prm  41991  lighneallem3  42003  lighneallem4b  42005  lighneallem4  42006  lighneal  42007  nn0o1gt2ALTV  42084  nn0oALTV  42086  odd2prm2  42106  even3prm2  42107  stgoldbwt  42143  sbgoldbwt  42144  sbgoldbalt  42148  sbgoldbo  42154  nnsum3primesgbe  42159  wtgoldbnnsum4prm  42169  bgoldbnnsum3prm  42171  bgoldbtbndlem2  42173  bgoldbtbndlem3  42174  bgoldbtbndlem4  42175  bgoldbtbnd  42176  bgoldbachlt  42180  tgblthelfgott  42182  bgoldbachltOLD  42186  tgblthelfgottOLD  42188  upgrwlkupwlk  42200  sprsymrelfolem2  42222  nrhmzr  42352  rngccatidALTV  42468  funcrngcsetcALT  42478  ringccatidALTV  42531  lincdifsn  42692  lindslinindimp2lem1  42726  lindsrng01  42736  ldepsnlinc  42776  m1modmmod  42795  blen1b  42861  nn0sumshdiglemB  42893  nn0sumshdiglem1  42894
  Copyright terms: Public domain W3C validator