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	|- ( ph -> ps )

Assertion

Ref	Expression
a1d	|- ( ph -> ( ch -> ps ) )

Proof of Theorem a1d

Step	Hyp	Ref	Expression
1		a1d.1	. 2 |- ( ph -> ps )
2		ax-1 6	. 2 |- ( ps -> ( ch -> ps ) )
3	1, 2	syl 17	1 |- ( ph -> ( ch -> ps ) )

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  330  adantr  481  jctild  566  jctird  567  pm3.4  584  anbi2d  740  anbi1d  741  ad4ant13  1292  ad4ant134  1296  meredith  1566  ax12  2304  ax12OLD  2341  nfsb4t  2389  ax12vALT  2428  moexex  2541  pm2.61da3ne  2883  ralrimivw  2967  reximdv  3016  rexlimdvw  3034  reuind  3411  sbcimdvOLD  3499  rexn0  4074  eqoreldifOLD  4226  tppreqb  4336  ssprsseq  4357  n0snor2el  4364  prnebg  4389  elpreqprlem  4395  3elpr2eq  4435  disjord  4641  disjiund  4643  axsep  4780  dtru  4857  propeqop  4970  propssopi  4971  fr0  5093  ssrel2  5210  poltletr  5528  ordsssuc2  5814  ordnbtwn  5816  ndmfv  6218  fveqres  6230  fmptco  6396  funsndifnop  6416  tpres  6466  fntpb  6473  elunirn  6509  isof1oopb  6575  fvmptopab  6697  ndmovord  6824  ordsucelsuc  7022  tfinds  7059  tfindsg  7060  limomss  7070  findsg  7093  finds1  7095  xpexr  7106  bropopvvv  7255  bropfvvvvlem  7256  bropfvvvv  7257  soxp  7290  suppun  7315  extmptsuppeq  7319  funsssuppss  7321  suppss  7325  suppssov1  7327  suppss2  7329  suppssfv  7331  mpt2xopynvov0  7344  smofvon2  7453  oaordi  7626  oawordeulem  7634  odi  7659  brdomg  7965  map1  8036  fopwdom  8068  fodomr  8111  mapxpen  8126  infensuc  8138  onomeneq  8150  fineqvlem  8174  fineqv  8175  xpfi  8231  finsschain  8273  fsuppun  8294  fsuppunbi  8296  funsnfsupp  8299  dffi3  8337  fisup2g  8374  fisupcl  8375  fiinf2g  8406  wemapso2  8458  en3lplem2  8512  inf3lemd  8524  r1ordg  8641  r1val1  8649  r1pw  8708  r1pwALT  8709  rankxplim3  8744  carddomi2  8796  fidomtri  8819  pr2ne  8828  alephon  8892  alephcard  8893  alephnbtwn  8894  alephordi  8897  iunfictbso  8937  fin23lem30  9164  fin1a2lem10  9231  axdc3lem2  9273  axdc3lem4  9275  alephval2  9394  cfpwsdom  9406  axextnd  9413  axrepnd  9416  axpownd  9423  axregnd  9426  axinfndlem1  9427  fpwwe2lem12  9463  wunfi  9543  addnidpi  9723  pinq  9749  mulgt0sr  9926  dedekind  10200  nnind  11038  nn1m1nn  11040  nn0n0n1ge2b  11359  nn0lt2  11440  nn0le2is012  11441  uzm1  11718  uzinfi  11768  nn01to3  11781  xrltnsym  11970  xrlttri  11972  xrlttr  11973  qbtwnxr  12031  xltnegi  12047  xnn0xaddcl  12066  xlt2add  12090  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  reltxrnmnf  12172  fzospliti  12500  elfzonlteqm1  12543  elfznelfzo  12573  injresinjlem  12588  injresinj  12589  modfzo0difsn  12742  addmodlteq  12745  ssnn0fi  12784  fsuppmapnn0fiub0  12793  suppssfz  12794  seqfveq2  12823  monoord  12831  seqf1o  12842  seqhomo  12848  faclbnd4lem4  13083  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashrabsn1  13163  hashgt0elex  13189  hash1snb  13207  hashf1lem2  13240  hashf1  13241  seqcoll  13248  hashle2pr  13259  pr2pwpr  13261  hashge2el2difr  13263  2swrd1eqwrdeq  13454  swrdswrd  13460  swrdccatin1  13483  swrdccatin12lem3  13490  swrdccat3  13492  swrdccat3blem  13495  repsdf2  13525  repswsymballbi  13527  cshw0  13540  cshwmodn  13541  cshwn  13543  cshwcl  13544  cshwlen  13545  cshw1  13568  2cshwcshw  13571  cshimadifsn  13575  s3sndisj  13706  s3iunsndisj  13707  relexprelg  13778  relexpnndm  13781  relexpaddg  13793  relexpaddd  13794  resqrex  13991  rexuz3  14088  rexanuz2  14089  limsupgre  14212  rlimconst  14275  caurcvg  14407  caucvg  14409  sumss  14455  fsumcl2lem  14462  modfsummods  14525  fsumrlim  14543  fsumo1  14544  fprodcl2lem  14680  dvdsaddre2b  15029  dvdsabseq  15035  mod2eq1n2dvds  15071  nno  15098  sumeven  15110  sumodd  15111  nn0seqcvgd  15283  lcmdvds  15321  lcmfunsnlem2  15353  lcmfunsnlem  15354  divgcdcoprm0  15379  exprmfct  15416  rpexp1i  15433  prm23lt5  15519  prm23ge5  15520  pcz  15585  pcadd  15593  pcmptcl  15595  oddprmdvds  15607  prmgaplem5  15759  prmgaplem6  15760  prmgaplem7  15761  cshwshashlem1  15802  cshwsdisj  15805  prmlem0  15812  setsstruct  15898  ressress  15938  initoeu2lem2  16665  mgm2nsgrplem2  17406  mgm2nsgrplem3  17407  dfgrp2e  17448  dfgrp3e  17515  symgextf1  17841  gsmsymgrfix  17848  gsmsymgreq  17852  sylow1lem1  18013  efgsf  18142  efgrelexlema  18162  dprdss  18428  ablfac1eulem  18471  lssssr  18953  01eq0ring  19272  psrvscafval  19390  mplcoe1  19465  mplcoe5  19468  mpfrcl  19518  psgnodpm  19934  mamudm  20194  matmulcell  20251  dmatmul  20303  scmatsgrp1  20328  mavmuldm  20356  mavmulsolcl  20357  mdetunilem9  20426  cramerlem3  20495  cramer0  20496  chpscmatgsumbin  20649  chp0mat  20651  fvmptnn04ifc  20657  fvmptnn04ifd  20658  epttop  20813  neiptopnei  20936  fiuncmp  21207  1stcrest  21256  comppfsc  21335  kgenss  21346  hmeofval  21561  fbun  21644  fgss2  21678  filuni  21689  filssufilg  21715  filufint  21724  hausflimi  21784  hausflim  21785  hauspwpwf1  21791  fclscmp  21834  alexsubALTlem4  21854  ptcmplem3  21858  ptcmplem5  21860  cstucnd  22088  isxmet2d  22132  imasdsf1olem  22178  blfps  22211  blf  22212  metrest  22329  nrginvrcn  22496  nmoge0  22525  nmoleub  22535  fsumcn  22673  cmetcaulem  23086  iscmet3  23091  iscmet2  23092  bcthlem2  23122  ovolicc2lem3  23287  itg2seq  23509  itg2splitlem  23515  itgeq1f  23538  itgeq2  23544  iblcnlem  23555  itgfsum  23593  limcnlp  23642  perfdvf  23667  dvnres  23694  dvmptfsum  23738  c1lip1  23760  abelth  24195  sinq12ge0  24260  rlimcnp  24692  xrlimcnp  24695  jensen  24715  ppiublem1  24927  dchrelbas3  24963  bcmono  25002  zabsle1  25021  gausslemma2dlem0f  25086  gausslemma2dlem1a  25090  gausslemma2dlem4  25094  lgsquad2lem2  25110  2lgslem1a1  25114  2lgslem3  25129  2lgs  25132  2lgsoddprm  25141  2sqlem10  25153  pntrsumbnd2  25256  pntpbnd1  25275  pntlem3  25298  axcontlem7  25850  ausgrusgrb  26060  usgredg2v  26119  lfuhgr1v0e  26146  subumgredg2  26177  upgrreslem  26196  umgrreslem  26197  fusgrfisbase  26220  nbuhgr  26239  uhgrnbgr0nb  26250  nbgr0vtxlem  26251  nbgr1vtx  26254  uvtxa0  26294  uvtx2vtx1edg  26299  cusgredg  26320  cusgrsizeinds  26348  sizusglecusg  26359  finsumvtxdg2size  26446  ewlkle  26501  upgriswlk  26537  pthdivtx  26625  usgr2trlncl  26656  crctcshwlkn0lem4  26705  wwlksn  26729  iswwlksnon  26740  iswspthsnon  26741  wwlksm1edg  26767  wwlksnfi  26801  wwlksnonfi  26816  wspn0  26820  2pthdlem1  26826  umgr2wlk  26845  clwwlksn  26881  clwlkclwwlklem2a  26899  clwlkclwwlk  26903  umgrclwwlksge2  26912  clwwlksnfi  26913  clwwisshclwws  26928  clwwnisshclwwsn  26930  3pthdlem1  27024  eupth2  27099  nfrgr2v  27136  frgr3vlem1  27137  1to2vfriswmgr  27143  1to3vfriswmgr  27144  vdgn1frgrv2  27160  frgrncvvdeqlem9  27171  frgrwopreglem4a  27174  frgrregorufr0  27188  frgrregorufr  27189  2wspmdisj  27201  extwwlkfab  27223  frgrreggt1  27251  frgrreg  27252  frgrregord13  27254  aevdemo  27317  shsvs  28182  0cnop  28838  0cnfn  28839  cnlnssadj  28939  ssmd1  29170  ssmd2  29171  atexch  29240  mdsymlem4  29265  sumdmdlem  29277  rabeqsnd  29342  ifeqeqx  29361  fmptcof2  29457  padct  29497  nnindf  29565  pwsiga  30193  ldsysgenld  30223  fiunelros  30237  breprexp  30711  bnj151  30947  bnj594  30982  bnj600  30989  subfacp1lem6  31167  erdszelem8  31180  cvmliftlem7  31273  cvmliftlem10  31276  cvmlift2lem12  31296  mrsubfval  31405  msubfval  31421  mclsssvlem  31459  trpredlem1  31727  poseq  31750  nolesgn2o  31824  funpartfv  32052  endofsegid  32192  broutsideof2  32229  a1i24  32295  nn0prpwlem  32317  nn0prpw  32318  ordcmp  32446  findreccl  32452  bj-alsb  32625  bj-ax6e  32653  bj-ax12v3ALT  32676  bj-axsep  32793  bj-dtru  32797  bj-xpnzex  32946  finxp00  33239  wl-spae  33306  wl-nfs1t  33324  poimirlem27  33436  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  itg2addnclem3  33463  itg2addnc  33464  ftc1anc  33493  areacirclem1  33500  sdclem2  33538  fdc  33541  mettrifi  33553  isexid2  33654  zerdivemp1x  33746  smprngopr  33851  mpt2bi123f  33971  mptbi12f  33975  ac6s6  33980  relcnveq3  34092  jca3  34140  ax12fromc15  34190  hbequid  34194  dvelimf-o  34214  ax12eq  34226  ax12el  34227  ax12indalem  34230  ax12inda2ALT  34231  ax12inda2  34232  lfl1dim  34408  lfl1dim2N  34409  lkreqN  34457  cvrexchlem  34705  ps-2  34764  paddasslem14  35119  idldil  35400  isltrn2N  35406  cdleme25a  35641  dibglbN  36455  dihlsscpre  36523  dvh4dimlem  36732  lcfl7N  36790  mapdval2N  36919  monotoddzzfi  37507  rp-fakeimass  37857  clublem  37917  relexpnul  37970  ee121  38711  ee122  38712  rspsbc2  38744  ax6e2ndeq  38775  vd12  38825  vd13  38826  ee221  38875  ee212  38877  ee112  38880  ee211  38883  ee210  38885  ee201  38887  ee120  38889  ee021  38891  ee012  38893  ee102  38895  ee03  38968  ee31  38979  ee31an  38981  ee123  38990  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  refsum2cnlem1  39196  fiiuncl  39234  eliin2f  39287  disjrnmpt2  39375  disjinfi  39380  rnmptbd2lem  39463  rnmptbdlem  39470  allbutfi  39616  infxrunb3rnmpt  39655  infrpgernmpt  39695  mccl  39830  constlimc  39856  limclner  39883  xlimmnfvlem1  40058  xlimpnfvlem1  40062  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvmptfprod  40160  dvnprodlem3  40163  stoweidlem31  40248  pwsal  40535  prsal  40538  sge0pnffigt  40613  sge0ltfirp  40617  0ome  40743  hoicvrrex  40770  hoidmvle  40814  ovnhoilem1  40815  ovnlecvr2  40824  smflimlem3  40981  reuan  41180  2reu4  41190  funressnfv  41208  ndmaovass  41286  otiunsndisjX  41298  nltle2tri  41323  fzoopth  41337  smonoord  41341  iccpartigtl  41359  icceuelpartlem  41371  iccpartnel  41374  pfxccat3  41426  fmtnoprmfac1  41477  fmtnoprmfac2  41479  prmdvdsfmtnof1lem2  41497  31prm  41512  lighneallem3  41524  lighneallem4b  41526  lighneallem4  41527  lighneal  41528  nn0o1gt2ALTV  41605  nn0oALTV  41607  odd2prm2  41627  even3prm2  41628  stgoldbwt  41664  sbgoldbwt  41665  sbgoldbalt  41669  sbgoldbo  41675  nnsum3primesgbe  41680  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  bgoldbachlt  41701  tgblthelfgott  41703  bgoldbachltOLD  41707  tgblthelfgottOLD  41709  upgrwlkupwlk  41721  sprsymrelfolem2  41743  nrhmzr  41873  rngccatidALTV  41989  funcrngcsetcALT  41999  ringccatidALTV  42052  lincdifsn  42213  lindslinindimp2lem1  42247  lindsrng01  42257  ldepsnlinc  42297  m1modmmod  42316  blen1b  42382  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415