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  2336  cbv1  2402  ralimdva  3144  reuss2  4276  ssrel  5723  ssrel2  5725  ssrelrel  5736  funfvima2  7165  isofrlem  7274  dfwe2  7707  tfindsg  7791  tfinds2  7794  tfinds3  7795  trom  7805  findsg  7827  finds2  7828  xpord3inddlem  8084  fpr3g  8215  wfr3g  8249  tfrlem1  8295  tfr3  8318  tz7.48lem  8360  oaordi  8461  oeordi  8502  nnaordi  8533  nnawordi  8536  naddssim  8600  naddoa  8617  nneneq  9115  ac6sfi  9168  fodomfi  9196  domunfican  9206  fodomfiOLD  9214  finsschain  9243  marypha1lem  9317  inf3lem2  9519  inf3lem5  9522  cantnfval2  9559  cantnflt  9562  cantnfp1lem3  9570  cnfcom  9590  ttrclss  9610  ttrclselem2  9616  frr3g  9646  dfac12lem3  10034  ackbij1lem16  10122  sornom  10165  infpssrlem4  10194  fin23lem34  10234  fin23lem36  10236  isf32lem1  10241  isf32lem2  10242  zorn2lem4  10387  zorn2lem5  10388  zorn2lem6  10389  zorn2lem7  10390  ttukeylem5  10401  pwfseqlem3  10548  wunfi  10609  grudomon  10705  prlem934  10921  sup2  12075  nnindd  12142  nnaddcl  12145  nnmulcl  12146  nnne0  12156  peano5uzi  12559  uzind2  12563  nn0indd  12567  fzind  12568  zindd  12571  fzindd  12572  uzaddcl  12799  uzwo  12806  om2uzlti  13854  seqcaopr3  13941  seqf1olem2a  13944  seqf1o  13947  ser1const  13962  expcllem  13976  expeq0  13996  mulexp  14005  expadd  14008  expmul  14011  expmordi  14071  leexp2r  14078  leexp1a  14079  bernneq  14133  modexp  14142  facdiv  14191  facwordi  14193  faclbnd  14194  faclbnd4lem4  14200  hashgadd  14281  hashmap  14339  hashf1lem2  14360  hashf1  14361  seqcoll  14368  cshweqrep  14725  relexpsucnnl  14934  relexpcnv  14939  relexpnndm  14945  relexpaddnn  14955  rlimsqzlem  15553  lo1le  15556  iseraltlem2  15587  fsum2d  15675  modfsummod  15698  fsumabs  15705  fsumrlim  15715  fsumo1  15716  fsumiun  15725  binom  15734  climcndslem1  15753  climcndslem2  15754  cvgrat  15787  clim2prod  15792  prodfn0  15798  prodfrec  15799  ntrivcvgfvn0  15803  fprodabs  15878  fprod2d  15885  binomfallfac  15945  bpolycl  15956  fprodefsum  15999  demoivreALT  16107  ruclem8  16143  ruclem9  16144  dvdsfac  16234  bitsinv1  16350  sadcadd  16366  sadadd2  16368  saddisjlem  16372  smuval2  16390  smupvallem  16391  smu01lem  16393  smupval  16396  smueqlem  16398  smumullem  16400  rplpwr  16466  nn0seqcvgd  16478  seq1st  16479  alginv  16483  algcvga  16487  algfx  16488  prmdvdsexp  16623  prmfac1  16628  eulerthlem2  16690  pcmpt  16801  pcfac  16808  prmpwdvds  16813  prmreclem4  16828  vdwlem10  16899  ramcl  16938  mreexexd  17551  frmdgsum  18767  mulgnnass  19019  mhmmulg  19025  gsumwrev  19276  gsmsymgrfix  19338  gsmsymgreq  19342  efginvrel2  19637  efgsrel  19644  gsum2dlem2  19881  ablfac1eulem  19984  pgpfac  19996  gsumle  20055  srgmulgass  20133  srgpcomp  20134  srgbinom  20147  lmodvsmmulgdi  20828  cnfldexp  21339  ofldchr  21511  assamulgscm  21836  mplcoe1  21970  mplcoe3  21971  mplcoe5  21973  mptcoe1fsupp  22126  coe1fzgsumdlem  22216  coe1fzgsumd  22217  gsummoncoe1  22221  evl1gsumdlem  22269  evl1gsumd  22270  mdetunilem9  22533  mptcoe1matfsupp  22715  mp2pm2mplem4  22722  chpdmat  22754  tgcl  22882  fiuncmp  23317  2ndcsep  23372  1stcelcls  23374  ptcmpfi  23726  tmdgsum  24008  fsumcn  24786  caubl  25233  caublcls  25234  ovolunlem1a  25422  ovolfiniun  25427  volfiniun  25473  voliunlem1  25476  volsuplem  25481  volsup  25482  dyadmax  25524  itgfsum  25753  dvnadd  25856  cpnord  25862  dvnfre  25881  dvmptfsum  25904  ply1divex  26067  fta1g  26100  plyco  26171  dgrcolem1  26204  dgrco  26206  dvnply2  26220  plydivex  26230  aaliou3lem2  26276  dvntaylp  26304  taylthlem1  26306  cxpmul2  26623  jensen  26924  ftalem2  27009  bcmono  27213  bposlem5  27224  lgsquad2lem2  27321  dchrisumlem1  27425  dchrisum0flb  27446  pntpbnd1  27522  pntlemf  27541  qabvle  27561  qabvexp  27562  ostthlem2  27564  ostth2lem2  27570  nosupbnd1lem5  27649  noinfbnd1lem5  27664  precsexlem8  28150  precsexlem9  28151  om2noseqrdg  28232  n0addscl  28270  n0mulscl  28271  eucliddivs  28299  peano5uzs  28326  expscllem  28351  expadds  28356  expsne0  28357  expsgt0  28358  pw2cut  28378  pw2cut2  28380  rusgrnumwwlk  29951  eupth2lems  30213  eupth2  30214  ipasslem1  30806  mdslmd1lem1  32300  mdslmd1lem2  32301  iuninc  32535  ssrelf  32593  nn0min  32798  nexple  32822  gsumwun  33040  gsumvsca1  33190  gsumvsca2  33191  domnprodn0  33237  unitprodclb  33349  1arithufdlem3  33506  cmppcmp  33866  esumfzf  34077  sseqp1  34403  rrvsum  34462  signstfvc  34582  bnj1174  35010  lfuhgr2  35151  subfacp1lem6  35217  mrsubvrs  35554  bccolsum  35771  iprodefisumlem  35772  faclimlem1  35775  onsuct0  36474  findfvcl  36485  poimirlem28  37687  sdclem2  37781  seqpo  37786  incsequz  37787  mettrifi  37796  heiborlem4  37853  bfplem1  37861  pclfinclN  39988  uzindd  42009  indstrd  42225  nnaddcom  42300  nnadddir  42302  nnmulcom  42304  sn-sup2  42523  incssnn0  42743  mzpexpmpt  42777  pell14qrexpclnn0  42898  monotuz  42973  rmxypos  42979  jm2.17a  42992  jm2.17b  42993  rmygeid  42996  jm2.18  43020  jm2.19lem3  43023  jm2.15nn0  43035  jm2.16nn0  43036  dfac11  43094  pwslnm  43126  hbtlem5  43160  cnsrexpcl  43197  cantnfresb  43356  onmcl  43363  naddonnn  43427  relexpxpnnidm  43735  relexpiidm  43736  relexpss1d  43737  iunrelexpmin1  43740  relexpmulnn  43741  iunrelexpmin2  43744  relexp0a  43748  trclimalb2  43758  dvgrat  44344  relpfrlem  44985  trfr  44994  lmodvsmdi  48409  tfis2d  49711