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  2338  cbv1  2407  ralimdva  3153  reuss2  4306  ssrel  5766  ssrelOLD  5767  ssrel2  5769  ssrelrel  5780  funfvima2  7228  isofrlem  7338  dfwe2  7773  tfindsg  7861  tfinds2  7864  tfinds3  7865  trom  7875  findsg  7898  finds2  7899  xpord3inddlem  8158  fpr3g  8289  wfr3g  8326  tfrlem1  8395  tfr3  8418  tz7.48lem  8460  oaordi  8563  oeordi  8604  nnaordi  8635  nnawordi  8638  naddssim  8702  naddoa  8719  nneneq  9225  ac6sfi  9297  fodomfi  9327  domunfican  9338  fodomfiOLD  9347  finsschain  9376  marypha1lem  9450  inf3lem2  9648  inf3lem5  9651  cantnfval2  9688  cantnflt  9691  cantnfp1lem3  9699  cnfcom  9719  ttrclss  9739  ttrclselem2  9745  frr3g  9775  dfac12lem3  10165  ackbij1lem16  10253  sornom  10296  infpssrlem4  10325  fin23lem34  10365  fin23lem36  10367  isf32lem1  10372  isf32lem2  10373  zorn2lem4  10518  zorn2lem5  10519  zorn2lem6  10520  zorn2lem7  10521  ttukeylem5  10532  pwfseqlem3  10679  wunfi  10740  grudomon  10836  prlem934  11052  sup2  12203  nnindd  12265  nnaddcl  12268  nnmulcl  12269  nnne0  12279  peano5uzi  12687  uzind2  12691  nn0indd  12695  fzind  12696  zindd  12699  fzindd  12700  uzaddcl  12925  uzwo  12932  om2uzlti  13973  seqcaopr3  14060  seqf1olem2a  14063  seqf1o  14066  ser1const  14081  expcllem  14095  expeq0  14115  mulexp  14124  expadd  14127  expmul  14130  expmordi  14190  leexp2r  14197  leexp1a  14198  bernneq  14252  modexp  14261  facdiv  14310  facwordi  14312  faclbnd  14313  faclbnd4lem4  14319  hashgadd  14400  hashmap  14458  hashf1lem2  14479  hashf1  14480  seqcoll  14487  cshweqrep  14844  relexpsucnnl  15054  relexpcnv  15059  relexpnndm  15065  relexpaddnn  15075  rlimsqzlem  15670  lo1le  15673  iseraltlem2  15704  fsum2d  15792  modfsummod  15815  fsumabs  15822  fsumrlim  15832  fsumo1  15833  fsumiun  15842  binom  15851  climcndslem1  15870  climcndslem2  15871  cvgrat  15904  clim2prod  15909  prodfn0  15915  prodfrec  15916  ntrivcvgfvn0  15920  fprodabs  15995  fprod2d  16002  binomfallfac  16062  bpolycl  16073  fprodefsum  16116  demoivreALT  16224  ruclem8  16260  ruclem9  16261  dvdsfac  16350  bitsinv1  16466  sadcadd  16482  sadadd2  16484  saddisjlem  16488  smuval2  16506  smupvallem  16507  smu01lem  16509  smupval  16512  smueqlem  16514  smumullem  16516  rplpwr  16582  nn0seqcvgd  16594  seq1st  16595  alginv  16599  algcvga  16603  algfx  16604  prmdvdsexp  16739  prmfac1  16744  eulerthlem2  16806  pcmpt  16917  pcfac  16924  prmpwdvds  16929  prmreclem4  16944  vdwlem10  17015  ramcl  17054  mreexexd  17665  frmdgsum  18845  mulgnnass  19097  mhmmulg  19103  gsumwrev  19354  gsmsymgrfix  19414  gsmsymgreq  19418  efginvrel2  19713  efgsrel  19720  gsum2dlem2  19957  ablfac1eulem  20060  pgpfac  20072  srgmulgass  20182  srgpcomp  20183  srgbinom  20196  lmodvsmmulgdi  20859  cnfldexp  21372  assamulgscm  21866  mplcoe1  22000  mplcoe3  22001  mplcoe5  22003  mptcoe1fsupp  22156  coe1fzgsumdlem  22246  coe1fzgsumd  22247  gsummoncoe1  22251  evl1gsumdlem  22299  evl1gsumd  22300  mdetunilem9  22563  mptcoe1matfsupp  22745  mp2pm2mplem4  22752  chpdmat  22784  tgcl  22912  fiuncmp  23347  2ndcsep  23402  1stcelcls  23404  ptcmpfi  23756  tmdgsum  24038  fsumcn  24817  caubl  25265  caublcls  25266  ovolunlem1a  25454  ovolfiniun  25459  volfiniun  25505  voliunlem1  25508  volsuplem  25513  volsup  25514  dyadmax  25556  itgfsum  25785  dvnadd  25888  cpnord  25894  dvnfre  25913  dvmptfsum  25936  ply1divex  26099  fta1g  26132  plyco  26203  dgrcolem1  26236  dgrco  26238  dvnply2  26252  plydivex  26262  aaliou3lem2  26308  dvntaylp  26336  taylthlem1  26338  cxpmul2  26655  jensen  26956  ftalem2  27041  bcmono  27245  bposlem5  27256  lgsquad2lem2  27353  dchrisumlem1  27457  dchrisum0flb  27478  pntpbnd1  27554  pntlemf  27573  qabvle  27593  qabvexp  27594  ostthlem2  27596  ostth2lem2  27602  nosupbnd1lem5  27681  noinfbnd1lem5  27696  precsexlem8  28173  precsexlem9  28174  om2noseqrdg  28255  n0addscl  28293  n0mulscl  28294  eucliddivs  28322  peano5uzs  28349  expscllem  28373  expadds  28377  expsne0  28378  expsgt0  28379  pw2cut  28392  rusgrnumwwlk  29962  eupth2lems  30224  eupth2  30225  ipasslem1  30817  mdslmd1lem1  32311  mdslmd1lem2  32312  iuninc  32546  ssrelf  32600  nn0min  32804  nexple  32828  gsumwun  33064  gsumle  33097  gsumvsca1  33228  gsumvsca2  33229  domnprodn0  33275  ofldchr  33341  unitprodclb  33409  1arithufdlem3  33566  cmppcmp  33894  esumfzf  34105  sseqp1  34432  rrvsum  34491  signstfvc  34611  bnj1174  35039  lfuhgr2  35146  subfacp1lem6  35212  mrsubvrs  35549  bccolsum  35761  iprodefisumlem  35762  faclimlem1  35765  onsuct0  36464  findfvcl  36475  poimirlem28  37677  sdclem2  37771  seqpo  37776  incsequz  37777  mettrifi  37786  heiborlem4  37843  bfplem1  37851  pclfinclN  39974  uzindd  41995  indstrd  42211  nnaddcom  42286  nnadddir  42288  nnmulcom  42290  sn-sup2  42489  incssnn0  42709  mzpexpmpt  42743  pell14qrexpclnn0  42864  monotuz  42940  rmxypos  42946  jm2.17a  42959  jm2.17b  42960  rmygeid  42963  jm2.18  42987  jm2.19lem3  42990  jm2.15nn0  43002  jm2.16nn0  43003  dfac11  43061  pwslnm  43093  hbtlem5  43127  cnsrexpcl  43164  cantnfresb  43323  onmcl  43330  naddonnn  43394  relexpxpnnidm  43702  relexpiidm  43703  relexpss1d  43704  iunrelexpmin1  43707  relexpmulnn  43708  iunrelexpmin2  43711  relexp0a  43715  trclimalb2  43725  dvgrat  44311  relpfrlem  44953  trfr  44962  lmodvsmdi  48334  tfis2d  49524