Theorem a2d 29

Description: Deduction distributing an embedded antecedent. Deduction form of ax-2 7. (Contributed by NM, 23-Jun-1994.)

Hypothesis

Ref	Expression
a2d.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
a2d	⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

Proof of Theorem a2d

Step	Hyp	Ref	Expression
1		a2d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2		ax-2 7	. 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:  mpdd  43  imim2d  57  imim3i  64  loowoz  112  animpimp2impd  864  minimp  1715  cbv1  2442  ralimdva  3161  reuss2  4119  ssrel  5422  ssrelOLD  5423  ssrel2  5425  ssrelrel  5435  funfvima2  6727  isofrlem  6823  dfwe2  7220  tfindsg  7299  tfinds2  7302  tfinds3  7303  ordom  7313  findsg  7332  finds2  7333  wfr3g  7657  tfrlem1  7717  tfr3  7740  tz7.48lem  7781  oaordi  7872  oeordi  7913  nnaordi  7944  nnawordi  7947  nneneq  8391  ac6sfi  8452  domunfican  8481  fodomfi  8487  finsschain  8521  marypha1lem  8587  inf3lem2  8782  inf3lem5  8785  cantnfval2  8822  cantnflt  8825  cantnfp1lem3  8833  cnfcom  8853  dfac12lem3  9261  ackbij1lem16  9351  sornom  9393  infpssrlem4  9422  fin23lem34  9462  fin23lem36  9464  isf32lem1  9469  isf32lem2  9470  zorn2lem4  9615  zorn2lem5  9616  zorn2lem6  9617  zorn2lem7  9618  ttukeylem5  9629  pwfseqlem3  9776  wunfi  9837  grudomon  9933  prlem934  10149  sup2  11273  nnaddcl  11338  nnmulcl  11339  nnmulclOLD  11340  peano5uzi  11751  uzind2  11755  nn0indd  11759  fzind  11760  zindd  11763  uzaddcl  11981  uzwo  11989  om2uzlti  12992  seqcaopr3  13078  seqf1olem2a  13081  seqf1o  13084  ser1const  13099  expcllem  13113  expeq0  13132  mulexp  13141  expadd  13144  expmul  13147  leexp2r  13160  leexp1a  13161  bernneq  13232  modexp  13241  facdiv  13313  facwordi  13315  faclbnd  13316  faclbnd4lem4  13322  faclbnd6  13325  hashgadd  13403  hashmap  13458  hashf1lem2  13476  hashf1  13477  seqcoll  13484  cshweqrep  13810  relexpsucnnl  14014  relexpcnv  14017  relexpnndm  14023  relexpaddnn  14033  cjexp  14132  absexp  14286  rlimsqzlem  14621  lo1le  14624  iseraltlem2  14655  fsum2d  14744  modfsummod  14767  fsumabs  14774  fsumrlim  14784  fsumo1  14785  fsumiun  14794  binom  14803  bcxmas  14808  climcndslem1  14822  climcndslem2  14823  cvgrat  14855  clim2prod  14860  prodfn0  14866  prodfrec  14867  ntrivcvgfvn0  14871  fprodabs  14944  fprod2d  14951  binomfallfac  15011  bpolycl  15022  fprodefsum  15064  demoivreALT  15170  ruclem8  15205  ruclem9  15206  dvdsfac  15290  bitsinv1  15402  sadcadd  15418  sadadd2  15420  saddisjlem  15424  smuval2  15442  smupvallem  15443  smu01lem  15445  smupval  15448  smueqlem  15450  smumullem  15452  gcdmultiple  15507  rplpwr  15514  nn0seqcvgd  15521  seq1st  15522  alginv  15526  algcvga  15530  algfx  15531  prmdvdsexp  15663  prmfac1  15667  eulerthlem2  15723  pcmpt  15832  pcfac  15839  prmpwdvds  15844  prmreclem4  15859  vdwlem10  15930  ramcl  15969  mreexexd  16532  frmdgsum  17623  mulgnnass  17798  mhmmulg  17804  gsumwrev  18016  gsmsymgrfix  18068  gsmsymgreq  18072  efginvrel2  18360  efgsrel  18367  gsum2dlem2  18590  ablfac1eulem  18692  pgpfac  18704  srgmulgass  18752  srgpcomp  18753  srgbinom  18766  lmodvsmmulgdi  19121  assamulgscm  19578  mplcoe1  19693  mplcoe3  19694  mplcoe5  19696  mptcoe1fsupp  19812  coe1fzgsumdlem  19898  coe1fzgsumd  19899  gsummoncoe1  19901  evl1gsumdlem  19947  evl1gsumd  19948  cnfldexp  20006  mdetunilem9  20657  mptcoe1matfsupp  20840  mp2pm2mplem4  20847  chpdmat  20879  tgcl  21007  fiuncmp  21441  2ndcsep  21496  1stcelcls  21498  ptcmpfi  21850  tmdmulg  22129  tmdgsum  22132  fsumcn  22906  caubl  23339  caublcls  23340  ovolunlem1a  23499  ovolfiniun  23504  volfiniun  23550  voliunlem1  23553  volsuplem  23558  volsup  23559  dyadmax  23601  itgfsum  23829  dvnadd  23928  cpnord  23934  dvnfre  23951  dvmptfsum  23974  ply1divex  24132  fta1g  24163  plyco  24233  dgrcolem1  24265  dgrco  24267  dvnply2  24278  plydivex  24288  aaliou3lem2  24334  dvntaylp  24361  taylthlem1  24363  cxpmul2  24671  jensen  24951  ftalem2  25036  bcmono  25238  bposlem5  25249  lgsquad2lem2  25346  dchrisumlem1  25414  dchrisum0flb  25435  pntpbnd1  25511  pntlemf  25530  qabvle  25550  qabvexp  25551  ostthlem2  25553  ostth2lem2  25559  rusgrnumwwlk  27139  eupth2lems  27433  eupth2  27434  ipasslem1  28036  mdslmd1lem1  29534  mdslmd1lem2  29535  iuninc  29726  ssrelf  29774  nnindd  29915  nn0min  29916  gsumle  30126  gsumvsca1  30129  gsumvsca2  30130  ofldchr  30161  cmppcmp  30272  nexple  30418  esumfzf  30478  sseqp1  30804  rrvsum  30863  signstfvc  30998  bnj1174  31415  subfacp1lem6  31511  mrsubvrs  31763  bccolsum  31968  iprodefisumlem  31969  faclimlem1  31972  trpredmintr  32072  frr3g  32121  nosupbnd1lem5  32200  onsuct0  32778  findfvcl  32789  bj-cbv1v  33064  poimirlem28  33768  sdclem2  33867  seqpo  33872  incsequz  33873  mettrifi  33882  heiborlem4  33942  bfplem1  33950  pclfinclN  35748  incssnn0  37793  mzpexpmpt  37827  pell14qrexpclnn0  37949  monotuz  38024  expmordi  38030  rmxypos  38032  jm2.17a  38045  jm2.17b  38046  rmygeid  38049  jm2.18  38073  jm2.19lem3  38076  jm2.15nn0  38088  jm2.16nn0  38089  dfac11  38150  pwslnm  38182  hbtlem5  38216  cnsrexpcl  38253  relexpxpnnidm  38512  relexpiidm  38513  relexpss1d  38514  iunrelexpmin1  38517  relexpmulnn  38518  iunrelexpmin2  38521  relexp0a  38525  trclimalb2  38535  dvgrat  39028  lmodvsmdi  42748  tfis2d  43012