Theorem a1d 26

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 18	1 ⊢ (𝜑 → (𝜒 → 𝜓))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  2a1d  27  a1i13  28  syl5com  32  mpid  45  syld  48  imim2d  58  syl6ci  72  syl5d  74  syl6d  76  pm2.21d  122  pm2.24d  152  conax1k  172  pm2.521g2  176  pm2.61iii  187  mtod  201  imbi2d  343  adantr  486  jctild  535  jctird  536  anbi2d  642  anbi1d  643  pm3.4  822  impsingle  1659  meredith  1673  stdpc4  2104  ax12  2452  ax12vALT  2498  nfsb4t  2528  moexexlem  2651  pm2.61da3ne  3044  ralrimivw  3158  rexlimdvw  3168  reximdv  3177  vtocl2d  3523  reuind  3710  reuan  3843  2reu4  4479  rabeqsnd  4626  tppreqb  4764  ssprsseq  4780  n0snor2el  4787  prnebg  4810  prel12g  4818  elpreqprlem  4820  3elpr2eq  4833  disjord  5091  disjiund  5093  dtruALT2  5331  exneq  5403  propssopi  5479  opthhausdorff  5489  fr0  5628  ssrel2  5760  poltletr  6125  reuop  6296  ordsssuc2  6456  ordnbtwn  6458  ndmfv  6918  fveqres  6930  fmptco  7131  funsndifnop  7156  tpres  7208  fntpb  7216  elunirn  7256  isof1oopb  7334  ndmovord  7612  ordsucelsuc  7834  tfinds  7872  tfindsg  7873  limomss  7883  findsg  7910  finds1  7912  xpexr  7931  resf1extb  7947  bropopvvv  8102  bropfvvvvlem  8103  bropfvvvv  8104  soxp  8144  poseq  8178  suppun  8205  extmptsuppeq  8209  funsssuppss  8211  suppss  8215  suppss2  8221  suppssfv  8223  suppco  8227  mpoxopynvov0  8239  smofvon2  8368  oaordi  8558  oawordeulem  8566  odi  8591  omeulem1  8594  brdomg  8989  snmapen  9070  fopwdom  9108  fodomr  9151  mapxpen  9166  infensuc  9178  fineqvlem  9261  fineqv  9262  fodomfir  9323  finsschain  9352  fsuppun  9383  fsuppunbi  9385  funsnfsupp  9388  dffi3  9427  fisup2g  9465  fisupcl  9466  fiinf2g  9498  infsupprpr  9502  wemapso2  9551  epnsym  9614  en3lplem2  9618  preleqg  9620  inf3lemd  9632  r1ordg  9789  r1val1  9797  r1pw  9863  r1pwALT  9864  rankxplim3  9902  eldju2ndl  10009  eldju2ndr  10010  carddomi2  10055  fidomtri  10078  alephon  10152  alephcard  10153  alephnbtwn  10154  alephordi  10157  iunfictbso  10197  fin23lem30  10424  fin1a2lem10  10491  axdc3lem2  10533  axdc3lem4  10535  alephval2  10661  cfpwsdom  10673  axextnd  10680  axrepnd  10683  axpownd  10690  axregnd  10693  axinfndlem1  10694  fpwwe2lem11  10730  wunfi  10810  addnidpi  10990  pinq  11016  mulgt0sr  11194  dedekind  11477  indval0  12328  nnind  12357  nn1m1nn  12360  nn0n0n1ge2b  12679  nn0lt2  12766  nn0le2is012  12767  uzm1  13003  uzinfi  13059  nn01to3  13072  xrltnsym  13270  xrlttri  13272  xrlttr  13273  qbtwnxr  13334  xltnegi  13350  xnn0xaddcl  13369  xlt2add  13394  xrsupsslem  13441  xrinfmsslem  13442  xrub  13446  reltxrnmnf  13477  fzdif1  13743  fzospliti  13830  elfzonlteqm1  13880  fzoopth  13901  elfznelfzo  13912  injresinjlem  13929  injresinj  13930  modfzo0difsn  14090  addmodlteq  14093  ssnn0fi  14132  fsuppmapnn0fiub0  14140  suppssfz  14141  seqfveq2  14171  monoord  14179  seqf1o  14190  seqhomo  14196  expnngt1  14389  faclbnd4lem4  14444  hasheqf1oi  14499  hashrabsn1  14522  hashgt0elex  14549  hash1snb  14568  hashf1lem2  14605  hashf1  14606  seqcoll  14613  hashle2pr  14626  pr2pwpr  14628  hashge2el2difr  14630  swrdnnn0nd  14811  swrdnd0  14812  pfxnd0  14843  swrdswrd  14859  pfxccatin12lem3  14886  pfxccat3  14888  swrdccat3blem  14893  repsdf2  14934  repswsymballbi  14936  cshw0  14950  cshwmodn  14951  cshwn  14953  cshwcl  14954  cshwlen  14955  cshw1  14978  2cshwcshw  14981  cshimadifsn  14985  s3sndisj  15126  s3iunsndisj  15127  relexprelg  15197  relexpnndm  15200  relexpaddg  15212  relexpaddd  15213  rtrclreclem4  15220  relexpindlem  15222  rexuz3  15522  rexanuz2  15523  limsupgre  15654  rlimconst  15717  caurcvg  15850  caucvg  15852  sumss  15896  fsumcl2lem  15903  modfsummods  15966  fsumrlim  15984  fsumo1  15985  fprodcl2lem  16123  dvdsaddre2b  16483  dvdsabseq  16489  mod2eq1n2dvds  16523  nno  16558  sumeven  16563  sumodd  16564  nn0rppwr  16741  nn0seqcvgd  16751  lcmdvds  16789  lcmfunsnlem2  16821  lcmfunsnlem  16822  divgcdcoprm0  16846  ge2nprmge4  16883  exprmfct  16886  rpexp1i  16905  prm23lt5  16998  prm23ge5  16999  pcz  17065  pcadd  17073  pcmptcl  17075  oddprmdvds  17087  prmgaplem6  17240  prmgaplem7  17241  cshwshashlem1  17279  cshwsdisj  17282  prmlem0  17289  setsstruct  17360  ressress  17431  initoeu2lem2  18196  mgmn0plusgf  18833  mgm2nsgrplem2  19124  mgm2nsgrplem3  19125  dfgrp2e  19180  dfgrp3e  19256  cyccom  19424  symgextf1  19641  gsmsymgrfix  19648  gsmsymgreq  19652  sylow1lem1  19818  efgsf  19949  efgrelexlema  19969  dprdss  20251  ablfac1eulem  20294  01eq0ringOLD  20788  nrhmzr  20795  funcrngcsetcALT  20899  lssssr  21235  isfieldidl  21546  psgnodpm  21900  psrvscafval  22262  mplcoe1  22352  mplcoe5  22355  mpfrcl  22400  mamudm  22716  matmulcell  22766  dmatmul  22818  scmatsgrp1  22843  mavmuldm  22871  mavmulsolcl  22872  mdetunilem9  22941  cramerlem3  23013  cramer0  23014  chpscmatgsumbin  23168  chp0mat  23170  fvmptnn04ifc  23176  fvmptnn04ifd  23177  epttop  23333  neiptopnei  23456  fiuncmp  23728  1stcrest  23777  kgenss  23868  hmeofval  24083  fbun  24165  fgss2  24199  filuni  24210  filssufilg  24236  filufint  24245  hausflimi  24305  hausflim  24306  hauspwpwf1  24312  fclscmp  24355  alexsubALTlem4  24375  ptcmplem3  24379  ptcmplem5  24381  cstucnd  24608  isxmet2d  24652  imasdsf1olem  24698  blfps  24731  blf  24732  metrest  24849  nrginvrcn  25017  nmoge0  25046  nmoleub  25056  fsumcn  25197  cmetcaulem  25615  iscmet3  25620  iscmet2  25621  bcthlem2  25652  ovolicc2lem3  25846  itg2seq  26069  itg2splitlem  26075  itgeq2  26104  iblcnlem  26115  itgfsum  26153  limcnlp  26204  perfdvf  26229  dvnres  26257  dvmptfsum  26301  c1lip1  26323  dvply2g  26612  taylply2  26701  abelth  26774  cxpsqrtth  27064  rlimcnp  27299  xrlimcnp  27302  jensen  27322  ppiublem1  27535  dchrelbas3  27571  bcmono  27610  zabsle1  27629  gausslemma2dlem0f  27694  gausslemma2dlem1a  27698  gausslemma2dlem4  27702  lgsquad2lem2  27718  2lgslem1a1  27722  2lgslem3  27737  2lgs  27740  2lgsoddprm  27749  2sqlem10  27761  2sqnn  27772  addsqnreup  27776  2sqreultblem  27781  2sqreunnltblem  27784  pntrsumbnd2  27900  pntpbnd1  27919  pntlem3  27942  fltoprmgt3  28002  nolesgn2o  28034  noetalem1  28104  bday0b  28205  leftf  28247  rightf  28248  oldss  28262  addcutslem  28369  negcut  28431  mulcutlem  28523  n0s0suc  28734  n0fincut  28747  n0s0m1  28754  nn1m1nns  28766  axcontlem7  29554  elntg2  29569  ausgrusgrb  29752  usgredg2v  29814  lfuhgr1v0e  29841  subumgredg2  29872  upgrreslem  29891  umgrreslem  29892  fusgrfisbase  29915  nbuhgr  29930  uhgrnbgr0nb  29941  nbgr0edglem  29943  nbgr1vtx  29945  cusgredg  30011  cusgrsizeinds  30039  sizusglecusg  30050  finsumvtxdg2size  30137  ewlkle  30192  upgriswlk  30227  pthdivtx  30318  dfpth2  30320  usgr2trlncl  30352  crctcshwlkn0lem4  30408  wwlksn  30432  iswwlksnon  30448  iswspthsnon  30451  wwlksm1edg  30476  wwlksnfi  30501  2pthdlem1  30525  umgr2wlk  30544  umgrclwwlkge2  30588  clwlkclwwlklem2a  30595  clwlkclwwlk  30599  clwlkclwwlkf1lem2  30602  clwlkclwwlkf  30605  clwwisshclwws  30612  clwwlknlbonbgr1  30636  clwwlknon0  30690  clwwlknonel  30692  clwwlknonex2e  30707  3pthdlem1  30771  eupth2  30846  nfrgr2v  30879  frgr3vlem1  30880  1to2vfriswmgr  30886  1to3vfriswmgr  30887  vdgn1frgrv2  30903  frgrncvvdeqlem9  30914  frgrwopreglem4a  30917  frgrregorufr0  30931  frgrregorufr  30932  2wspmdisj  30944  2clwwlk2clwwlklem  30953  frgrreggt1  31000  frgrreg  31001  frgrregord13  31003  aevdemo  31067  shsvs  31931  0cnop  32587  0cnfn  32588  cnlnssadj  32688  ssmd1  32919  ssmd2  32920  atexch  32989  mdsymlem4  33014  sumdmdlem  33026  ifeqeqx  33186  fmptcof2  33299  padct  33358  nnindf  33458  drng0mxidl  34047  constr01  34421  pwsiga  34809  pwldsys  34837  ldsysgenld  34840  fiunelros  34854  breprexp  35309  bnj151  35554  bnj594  35589  bnj600  35596  rmo6  35757  soinfdom  35769  trssfir1om  35790  rankscottu  35808  trssfir1omregs  35861  onf1oracwevd  35972  srepdflem2  36006  subfacp1lem6  36037  erdszelem8  36050  cvmliftlem7  36143  cvmliftlem10  36146  cvmlift2lem12  36166  sat1el2xp  36231  mrsubfval  36360  msubfval  36376  mclsssvlem  36414  antnestlaw2  36544  funpartfv  36802  endofsegid  36943  broutsideof2  36980  a1i24  37183  nn0prpwlem  37203  nn0prpw  37204  ordcmp  37328  findreccl  37334  axtcond  37359  dfttc2g  37387  dfttc4lem2  37410  bj-cbvaw  37633  bj-cbveaw  37635  bj-ax6e  37660  bj-ax12v3ALT  37681  bj-xpnzex  37965  bj-ideqg1  38179  rdgssun  38395  finxp00  38419  domalom  38421  isinf2  38422  fvineqsneq  38429  wl-spae  38547  wl-nfs1t  38563  poimirlem27  38659  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  itg2addnclem3  38685  itg2addnc  38686  ftc1anc  38713  areacirclem1  38720  sdclem2  38770  fdc  38773  mettrifi  38785  isexid2  38883  zerdivemp1x  38975  smprngopr  39080  mpobi123f  39188  mptbi12f  39192  ac6s6  39198  relcnveq3  39353  mopickr  39397  elrelscnveq3  39653  disjlem14  39927  jca3  40007  ax12fromc15  40056  hbequid  40060  dvelimf-o  40080  ax12eq  40092  ax12el  40093  ax12indalem  40096  ax12inda2ALT  40097  ax12inda2  40098  lfl1dim  40272  lfl1dim2N  40273  lkreqN  40321  cvrexchlem  40570  ps-2  40629  paddasslem14  40984  idldil  41265  isltrn2N  41271  cdleme25a  41504  dibglbN  42317  dihlsscpre  42385  dvh4dimlem  42594  lcfl7N  42652  mapdval2N  42781  dvrelog2b  43210  aks6d1c6lem3  43316  monotoddzzfi  44043  onov0suclim  44370  onmcl  44427  omabs2  44428  tfsconcat0b  44442  naddgeoa  44490  rp-fakeimass  44607  clublem  44704  grur1cld  45324  ee121  45582  ee122  45583  rspsbc2  45611  ax6e2ndeq  45636  vd12  45677  vd13  45678  ee221  45727  ee212  45729  ee112  45732  ee211  45735  ee210  45737  ee201  45739  ee120  45741  ee021  45743  ee012  45745  ee102  45747  ee03  45817  ee31  45828  ee31an  45830  ee123  45839  ax6e2ndeqVD  45985  ax6e2ndeqALT  46007  refsum2cnlem1  46148  fiiuncl  46176  eliin2f  46213  disjrnmpt2  46297  disjinfi  46301  rnmptbdlem  46361  allbutfi  46498  infxrunb3rnmpt  46532  infrpgernmpt  46569  monoordxrv  46585  mccl  46704  constlimc  46730  limclner  46755  xlimmnfvlem1  46936  xlimpnfvlem1  46940  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnprodlem3  47052  stoweidlem31  47135  pwsal  47419  prsal  47422  sge0pnffigt  47500  sge0ltfirp  47504  0ome  47633  hoicvrrex  47660  hoidmvle  47704  ovnhoilem1  47705  ovnlecvr2  47714  smflimlem3  47877  ormkglobd  47981  tmachlem-agreeprod  48041  funressnfv  48207  euoreqb  48273  ndmaovass  48370  afv2orxorb  48392  otiunsndisjX  48443  nltle2tri  48477  nnmul2b  48495  m1modmmod  48528  smonoord  48541  iccpartigtl  48599  icceuelpartlem  48611  iccpartnel  48614  sprsymrelfolem2  48669  prproropf1olem4  48682  paireqne  48687  reupr  48698  reuopreuprim  48702  nprmmul3  48705  fmtnoprmfac1  48744  fmtnoprmfac2  48746  prmdvdsfmtnof1lem2  48764  31prm  48776  lighneallem3  48786  lighneallem4b  48788  lighneallem4  48789  lighneal  48790  nprmdvdsfacm1lem2  48800  ppivalnnnprm  48807  nn0o1gt2ALTV  48886  nn0oALTV  48888  odd2prm2  48910  even3prm2  48911  fpprwppr  48931  stgoldbwt  48968  sbgoldbwt  48969  sbgoldbalt  48973  sbgoldbo  48979  nnsum3primesgbe  48984  wtgoldbnnsum4prm  48994  bgoldbnnsum3prm  48996  bgoldbtbndlem2  48998  bgoldbtbndlem3  48999  bgoldbtbndlem4  49000  bgoldbtbnd  49001  bgoldbachlt  49005  tgblthelfgott  49007  dfclnbgr6  49048  grimco  49081  uhgrimisgrgric  49123  grtriprop  49133  usgrgrtrirex  49142  isubgr3stgrlem6  49163  isubgr3stgrlem8  49165  grlimprclnbgr  49188  grlimgrtri  49195  gpgedg2ov  49258  gpg5nbgrvtx03starlem1  49260  gpg5nbgrvtx03starlem2  49261  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx13starlem1  49263  gpg5nbgrvtx13starlem2  49264  gpg5nbgrvtx13starlem3  49265  gpgcubic  49271  gpg5nbgr3star  49273  gpgprismgr4cycllem7  49293  pgnbgreunbgrlem2  49309  gpg5edgnedg  49322  upgrwlkupwlk  49332  rngccatidALTV  49463  ringccatidALTV  49497  lincdifsn  49630  lindslinindimp2lem1  49664  lindsrng01  49674  ldepsnlinc  49714  blen1b  49794  nn0sumshdiglemB  49826  nn0sumshdiglem1  49827  reorelicc  49916  rrx2plord2  49929  rrxlinesc  49942  line2ylem  49957  line2xlem  49959  thincmon  50662  thincepi  50663