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  847  minimp  1621  cbv1v  2338  cbv1  2407  ralimdva  3167  reuss2  4326  ssrel  5792  ssrelOLD  5793  ssrel2  5795  ssrelrel  5806  funfvima2  7251  isofrlem  7360  dfwe2  7794  tfindsg  7882  tfinds2  7885  tfinds3  7886  trom  7896  findsg  7919  finds2  7920  xpord3inddlem  8179  fpr3g  8310  wfr3g  8347  tfrlem1  8416  tfr3  8439  tz7.48lem  8481  oaordi  8584  oeordi  8625  nnaordi  8656  nnawordi  8659  naddssim  8723  naddoa  8740  nneneq  9246  nneneqOLD  9258  ac6sfi  9320  fodomfi  9350  domunfican  9361  fodomfiOLD  9370  finsschain  9399  marypha1lem  9473  inf3lem2  9669  inf3lem5  9672  cantnfval2  9709  cantnflt  9712  cantnfp1lem3  9720  cnfcom  9740  ttrclss  9760  ttrclselem2  9766  frr3g  9796  dfac12lem3  10186  ackbij1lem16  10274  sornom  10317  infpssrlem4  10346  fin23lem34  10386  fin23lem36  10388  isf32lem1  10393  isf32lem2  10394  zorn2lem4  10539  zorn2lem5  10540  zorn2lem6  10541  zorn2lem7  10542  ttukeylem5  10553  pwfseqlem3  10700  wunfi  10761  grudomon  10857  prlem934  11073  sup2  12224  nnindd  12286  nnaddcl  12289  nnmulcl  12290  nnne0  12300  peano5uzi  12707  uzind2  12711  nn0indd  12715  fzind  12716  zindd  12719  fzindd  12720  uzaddcl  12946  uzwo  12953  om2uzlti  13991  seqcaopr3  14078  seqf1olem2a  14081  seqf1o  14084  ser1const  14099  expcllem  14113  expeq0  14133  mulexp  14142  expadd  14145  expmul  14148  expmordi  14207  leexp2r  14214  leexp1a  14215  bernneq  14268  modexp  14277  facdiv  14326  facwordi  14328  faclbnd  14329  faclbnd4lem4  14335  hashgadd  14416  hashmap  14474  hashf1lem2  14495  hashf1  14496  seqcoll  14503  cshweqrep  14859  relexpsucnnl  15069  relexpcnv  15074  relexpnndm  15080  relexpaddnn  15090  rlimsqzlem  15685  lo1le  15688  iseraltlem2  15719  fsum2d  15807  modfsummod  15830  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fsumiun  15857  binom  15866  climcndslem1  15885  climcndslem2  15886  cvgrat  15919  clim2prod  15924  prodfn0  15930  prodfrec  15931  ntrivcvgfvn0  15935  fprodabs  16010  fprod2d  16017  binomfallfac  16077  bpolycl  16088  fprodefsum  16131  demoivreALT  16237  ruclem8  16273  ruclem9  16274  dvdsfac  16363  bitsinv1  16479  sadcadd  16495  sadadd2  16497  saddisjlem  16501  smuval2  16519  smupvallem  16520  smu01lem  16522  smupval  16525  smueqlem  16527  smumullem  16529  rplpwr  16595  nn0seqcvgd  16607  seq1st  16608  alginv  16612  algcvga  16616  algfx  16617  prmdvdsexp  16752  prmfac1  16757  eulerthlem2  16819  pcmpt  16930  pcfac  16937  prmpwdvds  16942  prmreclem4  16957  vdwlem10  17028  ramcl  17067  mreexexd  17691  frmdgsum  18875  mulgnnass  19127  mhmmulg  19133  gsumwrev  19385  gsmsymgrfix  19446  gsmsymgreq  19450  efginvrel2  19745  efgsrel  19752  gsum2dlem2  19989  ablfac1eulem  20092  pgpfac  20104  srgmulgass  20214  srgpcomp  20215  srgbinom  20228  lmodvsmmulgdi  20895  cnfldexp  21417  assamulgscm  21921  mplcoe1  22055  mplcoe3  22056  mplcoe5  22058  mptcoe1fsupp  22217  coe1fzgsumdlem  22307  coe1fzgsumd  22308  gsummoncoe1  22312  evl1gsumdlem  22360  evl1gsumd  22361  mdetunilem9  22626  mptcoe1matfsupp  22808  mp2pm2mplem4  22815  chpdmat  22847  tgcl  22976  fiuncmp  23412  2ndcsep  23467  1stcelcls  23469  ptcmpfi  23821  tmdgsum  24103  fsumcn  24894  caubl  25342  caublcls  25343  ovolunlem1a  25531  ovolfiniun  25536  volfiniun  25582  voliunlem1  25585  volsuplem  25590  volsup  25591  dyadmax  25633  itgfsum  25862  dvnadd  25965  cpnord  25971  dvnfre  25990  dvmptfsum  26013  ply1divex  26176  fta1g  26209  plyco  26280  dgrcolem1  26313  dgrco  26315  dvnply2  26329  plydivex  26339  aaliou3lem2  26385  dvntaylp  26413  taylthlem1  26415  cxpmul2  26731  jensen  27032  ftalem2  27117  bcmono  27321  bposlem5  27332  lgsquad2lem2  27429  dchrisumlem1  27533  dchrisum0flb  27554  pntpbnd1  27630  pntlemf  27649  qabvle  27669  qabvexp  27670  ostthlem2  27672  ostth2lem2  27678  nosupbnd1lem5  27757  noinfbnd1lem5  27772  precsexlem8  28238  precsexlem9  28239  om2noseqrdg  28310  n0addscl  28347  n0mulscl  28348  peano5uzs  28390  expscl  28413  expsne0  28414  expsgt0  28415  pw2cut  28420  rusgrnumwwlk  29995  eupth2lems  30257  eupth2  30258  ipasslem1  30850  mdslmd1lem1  32344  mdslmd1lem2  32345  iuninc  32573  ssrelf  32627  nn0min  32822  nexple  32833  gsumwun  33068  gsumle  33101  gsumvsca1  33232  gsumvsca2  33233  domnprodn0  33279  ofldchr  33344  unitprodclb  33417  1arithufdlem3  33574  cmppcmp  33857  esumfzf  34070  sseqp1  34397  rrvsum  34456  signstfvc  34589  bnj1174  35017  lfuhgr2  35124  subfacp1lem6  35190  mrsubvrs  35527  bccolsum  35739  iprodefisumlem  35740  faclimlem1  35743  onsuct0  36442  findfvcl  36453  poimirlem28  37655  sdclem2  37749  seqpo  37754  incsequz  37755  mettrifi  37764  heiborlem4  37821  bfplem1  37829  pclfinclN  39952  uzindd  41978  indstrd  42194  nnaddcom  42303  nnadddir  42305  nnmulcom  42307  sn-sup2  42501  incssnn0  42722  mzpexpmpt  42756  pell14qrexpclnn0  42877  monotuz  42953  rmxypos  42959  jm2.17a  42972  jm2.17b  42973  rmygeid  42976  jm2.18  43000  jm2.19lem3  43003  jm2.15nn0  43015  jm2.16nn0  43016  dfac11  43074  pwslnm  43106  hbtlem5  43140  cnsrexpcl  43177  cantnfresb  43337  onmcl  43344  naddonnn  43408  relexpxpnnidm  43716  relexpiidm  43717  relexpss1d  43718  iunrelexpmin1  43721  relexpmulnn  43722  iunrelexpmin2  43725  relexp0a  43729  trclimalb2  43739  dvgrat  44331  relpfrlem  44974  trfr  44979  lmodvsmdi  48295  tfis2d  49199