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  1621  cbv1v  2334  cbv1  2400  ralimdva  3145  reuss2  4289  ssrel  5745  ssrelOLD  5746  ssrel2  5748  ssrelrel  5759  funfvima2  7205  isofrlem  7315  dfwe2  7750  tfindsg  7837  tfinds2  7840  tfinds3  7841  trom  7851  findsg  7873  finds2  7874  xpord3inddlem  8133  fpr3g  8264  wfr3g  8298  tfrlem1  8344  tfr3  8367  tz7.48lem  8409  oaordi  8510  oeordi  8551  nnaordi  8582  nnawordi  8585  naddssim  8649  naddoa  8666  nneneq  9170  ac6sfi  9231  fodomfi  9261  domunfican  9272  fodomfiOLD  9281  finsschain  9310  marypha1lem  9384  inf3lem2  9582  inf3lem5  9585  cantnfval2  9622  cantnflt  9625  cantnfp1lem3  9633  cnfcom  9653  ttrclss  9673  ttrclselem2  9679  frr3g  9709  dfac12lem3  10099  ackbij1lem16  10187  sornom  10230  infpssrlem4  10259  fin23lem34  10299  fin23lem36  10301  isf32lem1  10306  isf32lem2  10307  zorn2lem4  10452  zorn2lem5  10453  zorn2lem6  10454  zorn2lem7  10455  ttukeylem5  10466  pwfseqlem3  10613  wunfi  10674  grudomon  10770  prlem934  10986  sup2  12139  nnindd  12206  nnaddcl  12209  nnmulcl  12210  nnne0  12220  peano5uzi  12623  uzind2  12627  nn0indd  12631  fzind  12632  zindd  12635  fzindd  12636  uzaddcl  12863  uzwo  12870  om2uzlti  13915  seqcaopr3  14002  seqf1olem2a  14005  seqf1o  14008  ser1const  14023  expcllem  14037  expeq0  14057  mulexp  14066  expadd  14069  expmul  14072  expmordi  14132  leexp2r  14139  leexp1a  14140  bernneq  14194  modexp  14203  facdiv  14252  facwordi  14254  faclbnd  14255  faclbnd4lem4  14261  hashgadd  14342  hashmap  14400  hashf1lem2  14421  hashf1  14422  seqcoll  14429  cshweqrep  14786  relexpsucnnl  14996  relexpcnv  15001  relexpnndm  15007  relexpaddnn  15017  rlimsqzlem  15615  lo1le  15618  iseraltlem2  15649  fsum2d  15737  modfsummod  15760  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  binom  15796  climcndslem1  15815  climcndslem2  15816  cvgrat  15849  clim2prod  15854  prodfn0  15860  prodfrec  15861  ntrivcvgfvn0  15865  fprodabs  15940  fprod2d  15947  binomfallfac  16007  bpolycl  16018  fprodefsum  16061  demoivreALT  16169  ruclem8  16205  ruclem9  16206  dvdsfac  16296  bitsinv1  16412  sadcadd  16428  sadadd2  16430  saddisjlem  16434  smuval2  16452  smupvallem  16453  smu01lem  16455  smupval  16458  smueqlem  16460  smumullem  16462  rplpwr  16528  nn0seqcvgd  16540  seq1st  16541  alginv  16545  algcvga  16549  algfx  16550  prmdvdsexp  16685  prmfac1  16690  eulerthlem2  16752  pcmpt  16863  pcfac  16870  prmpwdvds  16875  prmreclem4  16890  vdwlem10  16961  ramcl  17000  mreexexd  17609  frmdgsum  18789  mulgnnass  19041  mhmmulg  19047  gsumwrev  19298  gsmsymgrfix  19358  gsmsymgreq  19362  efginvrel2  19657  efgsrel  19664  gsum2dlem2  19901  ablfac1eulem  20004  pgpfac  20016  srgmulgass  20126  srgpcomp  20127  srgbinom  20140  lmodvsmmulgdi  20803  cnfldexp  21316  assamulgscm  21810  mplcoe1  21944  mplcoe3  21945  mplcoe5  21947  mptcoe1fsupp  22100  coe1fzgsumdlem  22190  coe1fzgsumd  22191  gsummoncoe1  22195  evl1gsumdlem  22243  evl1gsumd  22244  mdetunilem9  22507  mptcoe1matfsupp  22689  mp2pm2mplem4  22696  chpdmat  22728  tgcl  22856  fiuncmp  23291  2ndcsep  23346  1stcelcls  23348  ptcmpfi  23700  tmdgsum  23982  fsumcn  24761  caubl  25208  caublcls  25209  ovolunlem1a  25397  ovolfiniun  25402  volfiniun  25448  voliunlem1  25451  volsuplem  25456  volsup  25457  dyadmax  25499  itgfsum  25728  dvnadd  25831  cpnord  25837  dvnfre  25856  dvmptfsum  25879  ply1divex  26042  fta1g  26075  plyco  26146  dgrcolem1  26179  dgrco  26181  dvnply2  26195  plydivex  26205  aaliou3lem2  26251  dvntaylp  26279  taylthlem1  26281  cxpmul2  26598  jensen  26899  ftalem2  26984  bcmono  27188  bposlem5  27199  lgsquad2lem2  27296  dchrisumlem1  27400  dchrisum0flb  27421  pntpbnd1  27497  pntlemf  27516  qabvle  27536  qabvexp  27537  ostthlem2  27539  ostth2lem2  27545  nosupbnd1lem5  27624  noinfbnd1lem5  27639  precsexlem8  28116  precsexlem9  28117  om2noseqrdg  28198  n0addscl  28236  n0mulscl  28237  eucliddivs  28265  peano5uzs  28292  expscllem  28316  expadds  28320  expsne0  28321  expsgt0  28322  pw2cut  28335  rusgrnumwwlk  29905  eupth2lems  30167  eupth2  30168  ipasslem1  30760  mdslmd1lem1  32254  mdslmd1lem2  32255  iuninc  32489  ssrelf  32543  nn0min  32745  nexple  32769  gsumwun  33005  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  domnprodn0  33226  ofldchr  33292  unitprodclb  33360  1arithufdlem3  33517  cmppcmp  33848  esumfzf  34059  sseqp1  34386  rrvsum  34445  signstfvc  34565  bnj1174  34993  lfuhgr2  35106  subfacp1lem6  35172  mrsubvrs  35509  bccolsum  35726  iprodefisumlem  35727  faclimlem1  35730  onsuct0  36429  findfvcl  36440  poimirlem28  37642  sdclem2  37736  seqpo  37741  incsequz  37742  mettrifi  37751  heiborlem4  37808  bfplem1  37816  pclfinclN  39944  uzindd  41965  indstrd  42181  nnaddcom  42256  nnadddir  42258  nnmulcom  42260  sn-sup2  42479  incssnn0  42699  mzpexpmpt  42733  pell14qrexpclnn0  42854  monotuz  42930  rmxypos  42936  jm2.17a  42949  jm2.17b  42950  rmygeid  42953  jm2.18  42977  jm2.19lem3  42980  jm2.15nn0  42992  jm2.16nn0  42993  dfac11  43051  pwslnm  43083  hbtlem5  43117  cnsrexpcl  43154  cantnfresb  43313  onmcl  43320  naddonnn  43384  relexpxpnnidm  43692  relexpiidm  43693  relexpss1d  43694  iunrelexpmin1  43697  relexpmulnn  43698  iunrelexpmin2  43701  relexp0a  43705  trclimalb2  43715  dvgrat  44301  relpfrlem  44943  trfr  44952  lmodvsmdi  48367  tfis2d  49669