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  846  minimp  1622  cbv1v  2340  cbv1  2406  ralimdva  3148  reuss2  4278  ssrel  5732  ssrel2  5734  ssrelrel  5745  funfvima2  7177  isofrlem  7286  dfwe2  7719  tfindsg  7803  tfinds2  7806  tfinds3  7807  trom  7817  findsg  7839  finds2  7840  xpord3inddlem  8096  fpr3g  8227  wfr3g  8261  tfrlem1  8307  tfr3  8330  tz7.48lem  8372  oaordi  8473  oeordi  8515  nnaordi  8546  nnawordi  8549  naddssim  8613  naddoa  8630  nneneq  9130  ac6sfi  9184  fodomfi  9212  domunfican  9222  fodomfiOLD  9230  finsschain  9259  marypha1lem  9336  inf3lem2  9538  inf3lem5  9541  cantnfval2  9578  cantnflt  9581  cantnfp1lem3  9589  cnfcom  9609  ttrclss  9629  ttrclselem2  9635  frr3g  9668  dfac12lem3  10056  ackbij1lem16  10144  sornom  10187  infpssrlem4  10216  fin23lem34  10256  fin23lem36  10258  isf32lem1  10263  isf32lem2  10264  zorn2lem4  10409  zorn2lem5  10410  zorn2lem6  10411  zorn2lem7  10412  ttukeylem5  10423  pwfseqlem3  10571  wunfi  10632  grudomon  10728  prlem934  10944  sup2  12098  nnindd  12165  nnaddcl  12168  nnmulcl  12169  nnne0  12179  peano5uzi  12581  uzind2  12585  nn0indd  12589  fzind  12590  zindd  12593  fzindd  12594  uzaddcl  12817  uzwo  12824  om2uzlti  13873  seqcaopr3  13960  seqf1olem2a  13963  seqf1o  13966  ser1const  13981  expcllem  13995  expeq0  14015  mulexp  14024  expadd  14027  expmul  14030  expmordi  14090  leexp2r  14097  leexp1a  14098  bernneq  14152  modexp  14161  facdiv  14210  facwordi  14212  faclbnd  14213  faclbnd4lem4  14219  hashgadd  14300  hashmap  14358  hashf1lem2  14379  hashf1  14380  seqcoll  14387  cshweqrep  14744  relexpsucnnl  14953  relexpcnv  14958  relexpnndm  14964  relexpaddnn  14974  rlimsqzlem  15572  lo1le  15575  iseraltlem2  15606  fsum2d  15694  modfsummod  15717  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  binom  15753  climcndslem1  15772  climcndslem2  15773  cvgrat  15806  clim2prod  15811  prodfn0  15817  prodfrec  15818  ntrivcvgfvn0  15822  fprodabs  15897  fprod2d  15904  binomfallfac  15964  bpolycl  15975  fprodefsum  16018  demoivreALT  16126  ruclem8  16162  ruclem9  16163  dvdsfac  16253  bitsinv1  16369  sadcadd  16385  sadadd2  16387  saddisjlem  16391  smuval2  16409  smupvallem  16410  smu01lem  16412  smupval  16415  smueqlem  16417  smumullem  16419  rplpwr  16485  nn0seqcvgd  16497  seq1st  16498  alginv  16502  algcvga  16506  algfx  16507  prmdvdsexp  16642  prmfac1  16647  eulerthlem2  16709  pcmpt  16820  pcfac  16827  prmpwdvds  16832  prmreclem4  16847  vdwlem10  16918  ramcl  16957  mreexexd  17571  frmdgsum  18787  mulgnnass  19039  mhmmulg  19045  gsumwrev  19295  gsmsymgrfix  19357  gsmsymgreq  19361  efginvrel2  19656  efgsrel  19663  gsum2dlem2  19900  ablfac1eulem  20003  pgpfac  20015  gsumle  20074  srgmulgass  20152  srgpcomp  20153  srgbinom  20166  lmodvsmmulgdi  20848  cnfldexp  21359  ofldchr  21531  assamulgscm  21857  mplcoe1  21992  mplcoe3  21993  mplcoe5  21995  mptcoe1fsupp  22156  coe1fzgsumdlem  22247  coe1fzgsumd  22248  gsummoncoe1  22252  evl1gsumdlem  22300  evl1gsumd  22301  mdetunilem9  22564  mptcoe1matfsupp  22746  mp2pm2mplem4  22753  chpdmat  22785  tgcl  22913  fiuncmp  23348  2ndcsep  23403  1stcelcls  23405  ptcmpfi  23757  tmdgsum  24039  fsumcn  24817  caubl  25264  caublcls  25265  ovolunlem1a  25453  ovolfiniun  25458  volfiniun  25504  voliunlem1  25507  volsuplem  25512  volsup  25513  dyadmax  25555  itgfsum  25784  dvnadd  25887  cpnord  25893  dvnfre  25912  dvmptfsum  25935  ply1divex  26098  fta1g  26131  plyco  26202  dgrcolem1  26235  dgrco  26237  dvnply2  26251  plydivex  26261  aaliou3lem2  26307  dvntaylp  26335  taylthlem1  26337  cxpmul2  26654  jensen  26955  ftalem2  27040  bcmono  27244  bposlem5  27255  lgsquad2lem2  27352  dchrisumlem1  27456  dchrisum0flb  27477  pntpbnd1  27553  pntlemf  27572  qabvle  27592  qabvexp  27593  ostthlem2  27595  ostth2lem2  27601  nosupbnd1lem5  27680  noinfbnd1lem5  27695  precsexlem8  28210  precsexlem9  28211  om2noseqrdg  28300  n0addscl  28340  n0mulscl  28341  eucliddivs  28372  peano5uzs  28400  expscllem  28426  expadds  28431  expsne0  28432  expsgt0  28433  pw2cut  28456  pw2cut2  28458  rusgrnumwwlk  30051  eupth2lems  30313  eupth2  30314  ipasslem1  30906  mdslmd1lem1  32400  mdslmd1lem2  32401  iuninc  32635  ssrelf  32693  nn0min  32901  nexple  32925  gsumwun  33158  gsumvsca1  33308  gsumvsca2  33309  domnprodn0  33357  unitprodclb  33470  1arithufdlem3  33627  cmppcmp  34015  esumfzf  34226  sseqp1  34552  rrvsum  34611  signstfvc  34731  bnj1174  35159  lfuhgr2  35313  subfacp1lem6  35379  mrsubvrs  35716  bccolsum  35933  iprodefisumlem  35934  faclimlem1  35937  onsuct0  36635  findfvcl  36646  poimirlem28  37845  sdclem2  37939  seqpo  37944  incsequz  37945  mettrifi  37954  heiborlem4  38011  bfplem1  38019  pclfinclN  40206  uzindd  42227  indstrd  42443  nnaddcom  42519  nnadddir  42521  nnmulcom  42523  sn-sup2  42742  incssnn0  42949  mzpexpmpt  42983  pell14qrexpclnn0  43104  monotuz  43179  rmxypos  43185  jm2.17a  43198  jm2.17b  43199  rmygeid  43202  jm2.18  43226  jm2.19lem3  43229  jm2.15nn0  43241  jm2.16nn0  43242  dfac11  43300  pwslnm  43332  hbtlem5  43366  cnsrexpcl  43403  cantnfresb  43562  onmcl  43569  naddonnn  43633  relexpxpnnidm  43940  relexpiidm  43941  relexpss1d  43942  iunrelexpmin1  43945  relexpmulnn  43946  iunrelexpmin2  43949  relexp0a  43953  trclimalb2  43963  dvgrat  44549  relpfrlem  45190  trfr  45199  lmodvsmdi  48621  tfis2d  49921