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

Step	Hyp	Ref	Expression
1		a1d.1	. 2 ⊢ (𝜑 → 𝜓)
2		ax-1 6	. 2 ⊢ (𝜓 → (𝜒 → 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 → 𝜓))

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  43  syld  46  imim2d  55  syl6ci  69  syl5d  71  syl6d  73  pm2.21d  117  pm2.24d  146  pm2.51  164  pm2.521  165  pm2.61iii  178  mtod  188  impbid21d  200  imbi2d  329  adantr  480  jctild  564  jctird  565  pm3.4  582  anbi2d  736  anbi1d  737  ad4ant13  1284  ad4ant134  1288  meredith  1557  ax12  2292  ax12OLD  2329  nfsb4t  2377  ax12vALT  2416  moexex  2529  pm2.61da3ne  2871  ralrimivw  2950  reximdv  2999  rexlimdvw  3016  reuind  3378  sbcimdvOLD  3466  rexn0  4026  eqoreldifOLD  4173  tppreqb  4277  ssprsseq  4297  n0snor2el  4304  prnebg  4329  elpreqprlem  4333  axsep  4708  dtru  4783  propeqop  4895  propssopi  4896  fr0  5017  ssrel2  5133  poltletr  5447  ordsssuc2  5731  ordnbtwn  5733  ndmfv  6128  fveqres  6140  fmptco  6303  funsndifnop  6321  tpres  6371  fntpb  6378  elunirn  6413  isof1oopb  6475  ndmovord  6722  ordsucelsuc  6914  tfinds  6951  tfindsg  6952  limomss  6962  findsg  6985  finds1  6987  xpexr  6999  bropopvvv  7142  bropfvvvvlem  7143  bropfvvvv  7144  soxp  7177  suppun  7202  extmptsuppeq  7206  funsssuppss  7208  suppss  7212  suppssov1  7214  suppss2  7216  suppssfv  7218  mpt2xopynvov0  7231  smofvon2  7340  oaordi  7513  oawordeulem  7521  odi  7546  brdomg  7851  map1  7921  fopwdom  7953  fodomr  7996  mapxpen  8011  infensuc  8023  onomeneq  8035  fineqvlem  8059  fineqv  8060  xpfi  8116  finsschain  8156  fsuppun  8177  fsuppunbi  8179  funsnfsupp  8182  dffi3  8220  fisup2g  8257  fisupcl  8258  fiinf2g  8289  wemapso2  8341  en3lplem2  8395  inf3lemd  8407  r1ordg  8524  r1val1  8532  r1pw  8591  r1pwALT  8592  rankxplim3  8627  carddomi2  8679  fidomtri  8702  pr2ne  8711  alephon  8775  alephcard  8776  alephnbtwn  8777  alephordi  8780  iunfictbso  8820  fin23lem30  9047  fin1a2lem10  9114  axdc3lem2  9156  axdc3lem4  9158  alephval2  9273  cfpwsdom  9285  axextnd  9292  axrepnd  9295  axpownd  9302  axregnd  9305  axinfndlem1  9306  fpwwe2lem12  9342  wunfi  9422  addnidpi  9602  pinq  9628  mulgt0sr  9805  dedekind  10079  nnind  10915  nn1m1nn  10917  nn0n0n1ge2b  11236  nn0lt2  11317  uzm1  11594  uzinfi  11644  nn01to3  11657  xrltnsym  11846  xrlttri  11848  xrlttr  11849  qbtwnxr  11905  xltnegi  11921  xnn0xaddcl  11940  xlt2add  11962  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  reltxrnmnf  12043  fzospliti  12369  elfzonlteqm1  12410  elfznelfzo  12439  injresinjlem  12450  injresinj  12451  modfzo0difsn  12604  addmodlteq  12607  ssnn0fi  12646  fsuppmapnn0fiub0  12655  suppssfz  12656  seqfveq2  12685  seqshft2  12689  monoord  12693  seqsplit  12696  seqf1o  12704  seqhomo  12710  faclbnd4lem4  12945  hasheqf1oi  13002  hasheqf1oiOLD  13003  hashrabsn1  13024  hashgt0elex  13050  hash1snb  13068  hashf1lem2  13097  hashf1  13098  seqcoll  13105  pr2pwpr  13116  hashge2el2difr  13118  fundmge2nop0  13129  2swrd1eqwrdeq  13306  swrdswrd  13312  swrdccatin1  13334  swrdccatin12lem3  13341  swrdccat3  13343  swrdccat3blem  13346  repsdf2  13376  repswsymballbi  13378  cshw0  13391  cshwmodn  13392  cshwn  13394  cshwcl  13395  cshwlen  13396  cshw1  13419  2cshwcshw  13422  cshimadifsn  13426  s3sndisj  13554  s3iunsndisj  13555  relexprelg  13626  relexpnndm  13629  relexpaddg  13641  relexpaddd  13642  resqrex  13839  rexuz3  13936  rexanuz2  13937  limsupgre  14060  rlimconst  14123  caurcvg  14255  caucvg  14257  sumss  14302  fsumcl2lem  14309  modfsummods  14366  fsumrlim  14384  fsumo1  14385  fprodcl2lem  14519  dvdsaddre2b  14867  dvdsabseq  14873  zeneo  14901  mod2eq1n2dvds  14909  nno  14936  sumeven  14948  sumodd  14949  nn0seqcvgd  15121  lcmdvds  15159  lcmfunsnlem2  15191  lcmfunsnlem  15192  divgcdcoprm0  15217  exprmfct  15254  rpexp1i  15271  prm23lt5  15357  prm23ge5  15358  pcz  15423  pcadd  15431  pcmptcl  15433  oddprmdvds  15445  prmgaplem5  15597  prmgaplem6  15598  prmgaplem7  15599  cshwshashlem1  15640  cshwsdisj  15643  prmlem0  15650  ressress  15765  initoeu2lem2  16488  mgm2nsgrplem2  17229  mgm2nsgrplem3  17230  dfgrp2e  17271  dfgrp3e  17338  symgextf1  17664  gsmsymgrfix  17671  gsmsymgreq  17675  sylow1lem1  17836  efgsf  17965  efgrelexlema  17985  dprdss  18251  ablfac1eulem  18294  lssssr  18774  01eq0ring  19093  psrvscafval  19211  mplcoe1  19286  mplcoe5  19289  mpfrcl  19339  psgnodpm  19753  mamudm  20013  matmulcell  20070  dmatmul  20122  scmatsgrp1  20147  mavmuldm  20175  mavmulsolcl  20176  mdetunilem9  20245  cramerlem3  20314  cramer0  20315  chpscmatgsumbin  20468  chp0mat  20470  fvmptnn04ifc  20476  fvmptnn04ifd  20477  epttop  20623  neiptopnei  20746  fiuncmp  21017  1stcrest  21066  comppfsc  21145  kgenss  21156  hmeofval  21371  fbun  21454  fgss2  21488  filuni  21499  filssufilg  21525  filufint  21534  hausflimi  21594  hausflim  21595  hauspwpwf1  21601  fclscmp  21644  alexsubALTlem4  21664  ptcmplem3  21668  ptcmplem5  21670  cstucnd  21898  isxmet2d  21942  imasdsf1olem  21988  blfps  22021  blf  22022  metrest  22139  nrginvrcn  22306  nmoge0  22335  nmoleub  22345  fsumcn  22481  cmetcaulem  22894  iscmet3  22899  iscmet2  22900  bcthlem2  22930  ovolicc2lem3  23094  itg2seq  23315  itg2splitlem  23321  itgeq1f  23344  itgeq2  23350  iblcnlem  23361  itgfsum  23399  limcnlp  23448  perfdvf  23473  dvnres  23500  dvmptfsum  23542  c1lip1  23564  abelth  23999  sinq12ge0  24064  rlimcnp  24492  xrlimcnp  24495  jensen  24515  ppiublem1  24727  dchrelbas3  24763  bcmono  24802  zabsle1  24821  gausslemma2dlem0f  24886  gausslemma2dlem1a  24890  gausslemma2dlem4  24894  lgsquad2lem2  24910  2lgslem1a1  24914  2lgslem3  24929  2lgs  24932  2lgsoddprm  24941  2sqlem10  24953  pntrsumbnd2  25056  pntpbnd1  25075  pntlem3  25098  axcontlem7  25650  ausisusgra  25884  usgraidx2v  25922  nbgra0nb  25958  nbgranself2  25965  nbgraf1olem3  25972  nbgraf1olem5  25974  nb3graprlem1  25980  nbcusgra  25992  cusgrasizeinds  26004  usgra2wlkspthlem1  26147  wwlkm1edg  26263  wwlknfi  26266  clwwlkprop  26298  clwwlknprop  26300  clwlkisclwwlklem2a  26313  el2wlkonotot0  26399  usg2wlkonot  26410  usg2wotspth  26411  2spontn0vne  26414  vdgrf  26425  cusgraiffrusgra  26467  rusgraprop4  26471  rusgrasn  26472  eupai  26494  eupath2  26507  frgra2v  26526  frgra3vlem1  26527  3vfriswmgralem  26531  1to2vfriswmgra  26533  1to3vfriswmgra  26534  2pthfrgra  26538  vdfrgra0  26549  vdgn1frgrav2  26553  frgrawopreglem2  26572  frgrawopreglem3  26573  frgrawopreglem4  26574  frgrawopreg  26576  frgraregorufr0  26579  frgraregorufr  26580  2spotdisj  26588  2spotiundisj  26589  2spotmdisj  26595  numclwwlkovf2ex  26613  extwwlkfab  26617  frgrareggt1  26643  frgrareg  26644  frgraregord13  26646  aevdemo  26709  shsvs  27566  0cnop  28222  0cnfn  28223  cnlnssadj  28323  ssmd1  28554  ssmd2  28555  atexch  28624  mdsymlem4  28649  sumdmdlem  28661  ifeqeqx  28745  fmptcof2  28839  padct  28885  nnindf  28952  pwsiga  29520  ldsysgenld  29550  fiunelros  29564  bnj151  30201  bnj594  30236  bnj600  30243  subfacp1lem6  30421  erdszelem8  30434  cvmliftlem7  30527  cvmliftlem10  30530  cvmlift2lem12  30550  mrsubfval  30659  msubfval  30675  mclsssvlem  30713  trpredlem1  30971  poseq  30994  funpartfv  31222  endofsegid  31362  broutsideof2  31399  a1i24  31465  nn0prpwlem  31487  nn0prpw  31488  ordcmp  31616  findreccl  31622  bj-alsb  31814  bj-ax6e  31842  bj-ax12v3ALT  31863  bj-axsep  31981  bj-dtru  31985  bj-xpnzex  32139  bj-xnex  32245  finxp00  32415  wl-spae  32485  wl-nfs1t  32503  poimirlem27  32606  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  itg2addnclem3  32633  itg2addnc  32634  ftc1anc  32663  areacirclem1  32670  sdclem2  32708  fdc  32711  mettrifi  32723  isexid2  32824  zerdivemp1x  32916  smprngopr  33021  mpt2bi123f  33141  mptbi12f  33145  ac6s6  33150  jca3  33156  ax12fromc15  33208  hbequid  33212  dvelimf-o  33232  ax12eq  33244  ax12el  33245  ax12indalem  33248  ax12inda2ALT  33249  ax12inda2  33250  lfl1dim  33426  lfl1dim2N  33427  lkreqN  33475  cvrexchlem  33723  ps-2  33782  paddasslem14  34137  idldil  34418  isltrn2N  34424  cdleme25a  34659  dibglbN  35473  dihlsscpre  35541  dvh4dimlem  35750  lcfl7N  35808  mapdval2N  35937  monotoddzzfi  36525  rp-fakeimass  36876  clublem  36936  relexpnul  36989  ee121  37732  ee122  37733  rspsbc2  37765  ax6e2ndeq  37796  vd12  37846  vd13  37847  ee221  37896  ee212  37898  ee112  37901  ee211  37904  ee210  37906  ee201  37908  ee120  37910  ee021  37912  ee012  37914  ee102  37916  ee03  37989  ee31  38000  ee31an  38002  ee123  38011  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  refsum2cnlem1  38219  fiiuncl  38259  eliin2f  38316  disjrnmpt2  38370  disjinfi  38375  allbutfi  38557  mccl  38665  constlimc  38691  limclner  38718  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvmptfprod  38835  dvnprodlem3  38838  stoweidlem31  38924  pwsal  39211  prsal  39214  sge0pnffigt  39289  sge0ltfirp  39293  0ome  39419  hoicvrrex  39446  hoidmvle  39490  ovnhoilem1  39491  ovnlecvr2  39500  smflimlem3  39659  reuan  39829  2reu4  39839  funressnfv  39857  ndmaovass  39935  nltle2tri  39942  smonoord  39944  iccpartigtl  39961  icceuelpartlem  39973  iccpartnel  39976  fmtnoprmfac1  40015  fmtnoprmfac2  40017  prmdvdsfmtnof1lem2  40035  31prm  40050  lighneallem3  40062  lighneallem4b  40064  lighneallem4  40065  lighneal  40066  nn0o1gt2ALTV  40143  nn0oALTV  40145  stgoldbwt  40198  bgoldbwt  40199  sgoldbalt  40203  nnsum3primesgbe  40208  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  bgoldbachlt  40227  tgblthelfgott  40229  bgoldbachltOLD  40234  tgblthelfgottOLD  40236  pfxccat3  40289  otiunsndisjX  40317  fzoopth  40360  ausgrusgrb  40395  usgredg2v  40454  lfuhgr1v0e  40480  subumgredg2  40509  fusgrfisbase  40547  nbuhgr  40565  uhgrnbgr0nb  40576  nbgr0vtxlem  40577  nbgr1vtx  40580  uvtxa0  40620  uvtx2vtx1edg  40625  cusgredg  40646  cusgrsizeinds  40668  sizusglecusg  40679  ewlkle  40807  upgr1wlkwlk  40847  pthdivtx  40935  usgr2trlncl  40966  cyclnsPth  41006  crctcsh1wlkn0lem4  41016  wwlksn  41040  iswwlksnon  41051  iswspthsnon  41052  wwlksm1edg  41078  wwlksnfi  41112  wwlksnonfi  41127  wspn0  41131  2pthdlem1  41137  umgr2wlk  41156  2wspdisj  41165  2wspiundisj  41166  clwwlksn  41189  clwlkclwwlklem2a  41207  clwlkclwwlk  41211  umgrclwwlksge2  41219  clwwlksnfi  41220  clwwisshclwws  41235  clwwnisshclwwsn  41237  3pthdlem1  41331  eupth2  41407  nfrgr2v  41442  frgr3vlem1  41443  1to2vfriswmgr  41449  1to3vfriswmgr  41450  vdgn1frgrv2  41466  frgrwopreglem3  41483  frgrwopreglem4  41484  frgrwopreg  41486  frgrregorufr0  41489  frgrregorufr  41490  fusgr2wsp2nb  41498  2wspmdisj  41501  av-numclwwlkovf2ex  41517  av-extwwlkfab  41520  av-frgrareggt1  41547  av-frgrareg  41548  av-frgraregord13  41550  nrhmzr  41663  rngccatidALTV  41781  funcrngcsetcALT  41791  ringccatidALTV  41844  nn0le2is012  41938  lincdifsn  42007  lindslinindimp2lem1  42041  lindsrng01  42051  ldepsnlinc  42091  m1modmmod  42110  blen1b  42180  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213