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  842  minimp  1625  cbv1v  2335  cbv1  2402  ralimdva  3102  reuss2  4246  ssrel  5683  ssrel2  5685  ssrelrel  5695  funfvima2  7089  isofrlem  7191  dfwe2  7602  tfindsg  7682  tfinds2  7685  tfinds3  7686  trom  7696  findsg  7720  finds2  7721  fpr3g  8072  wfr3g  8109  tfrlem1  8178  tfr3  8201  tz7.48lem  8242  oaordi  8339  oeordi  8380  nnaordi  8411  nnawordi  8414  nneneq  8896  ac6sfi  8988  domunfican  9017  fodomfi  9022  finsschain  9056  marypha1lem  9122  inf3lem2  9317  inf3lem5  9320  cantnfval2  9357  cantnflt  9360  cantnfp1lem3  9368  cnfcom  9388  trpredmintr  9409  frr3g  9445  dfac12lem3  9832  ackbij1lem16  9922  sornom  9964  infpssrlem4  9993  fin23lem34  10033  fin23lem36  10035  isf32lem1  10040  isf32lem2  10041  zorn2lem4  10186  zorn2lem5  10187  zorn2lem6  10188  zorn2lem7  10189  ttukeylem5  10200  pwfseqlem3  10347  wunfi  10408  grudomon  10504  prlem934  10720  sup2  11861  nnindd  11923  nnaddcl  11926  nnmulcl  11927  nnne0  11937  peano5uzi  12339  uzind2  12343  nn0indd  12347  fzind  12348  zindd  12351  uzaddcl  12573  uzwo  12580  om2uzlti  13598  seqcaopr3  13686  seqf1olem2a  13689  seqf1o  13692  ser1const  13707  expcllem  13721  expeq0  13741  mulexp  13750  expadd  13753  expmul  13756  expmordi  13813  leexp2r  13820  leexp1a  13821  bernneq  13872  modexp  13881  facdiv  13929  facwordi  13931  faclbnd  13932  faclbnd4lem4  13938  hashgadd  14020  hashmap  14078  hashf1lem2  14098  hashf1  14099  seqcoll  14106  cshweqrep  14462  relexpsucnnl  14669  relexpcnv  14674  relexpnndm  14680  relexpaddnn  14690  rlimsqzlem  15288  lo1le  15291  iseraltlem2  15322  fsum2d  15411  modfsummod  15434  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  binom  15470  climcndslem1  15489  climcndslem2  15490  cvgrat  15523  clim2prod  15528  prodfn0  15534  prodfrec  15535  ntrivcvgfvn0  15539  fprodabs  15612  fprod2d  15619  binomfallfac  15679  bpolycl  15690  fprodefsum  15732  demoivreALT  15838  ruclem8  15874  ruclem9  15875  dvdsfac  15963  bitsinv1  16077  sadcadd  16093  sadadd2  16095  saddisjlem  16099  smuval2  16117  smupvallem  16118  smu01lem  16120  smupval  16123  smueqlem  16125  smumullem  16127  gcdmultipleOLD  16188  rplpwr  16195  nn0seqcvgd  16203  seq1st  16204  alginv  16208  algcvga  16212  algfx  16213  prmdvdsexp  16348  prmfac1  16354  eulerthlem2  16411  pcmpt  16521  pcfac  16528  prmpwdvds  16533  prmreclem4  16548  vdwlem10  16619  ramcl  16658  mreexexd  17274  frmdgsum  18416  mulgnnass  18653  mhmmulg  18659  gsumwrev  18888  gsmsymgrfix  18951  gsmsymgreq  18955  efginvrel2  19248  efgsrel  19255  gsum2dlem2  19487  ablfac1eulem  19590  pgpfac  19602  srgmulgass  19682  srgpcomp  19683  srgbinom  19696  lmodvsmmulgdi  20073  cnfldexp  20543  assamulgscm  21015  mplcoe1  21148  mplcoe3  21149  mplcoe5  21151  mptcoe1fsupp  21296  coe1fzgsumdlem  21382  coe1fzgsumd  21383  gsummoncoe1  21385  evl1gsumdlem  21432  evl1gsumd  21433  mdetunilem9  21677  mptcoe1matfsupp  21859  mp2pm2mplem4  21866  chpdmat  21898  tgcl  22027  fiuncmp  22463  2ndcsep  22518  1stcelcls  22520  ptcmpfi  22872  tmdgsum  23154  fsumcn  23939  caubl  24377  caublcls  24378  ovolunlem1a  24565  ovolfiniun  24570  volfiniun  24616  voliunlem1  24619  volsuplem  24624  volsup  24625  dyadmax  24667  itgfsum  24896  dvnadd  24998  cpnord  25004  dvnfre  25021  dvmptfsum  25044  ply1divex  25206  fta1g  25237  plyco  25307  dgrcolem1  25339  dgrco  25341  dvnply2  25352  plydivex  25362  aaliou3lem2  25408  dvntaylp  25435  taylthlem1  25437  cxpmul2  25749  jensen  26043  ftalem2  26128  bcmono  26330  bposlem5  26341  lgsquad2lem2  26438  dchrisumlem1  26542  dchrisum0flb  26563  pntpbnd1  26639  pntlemf  26658  qabvle  26678  qabvexp  26679  ostthlem2  26681  ostth2lem2  26687  rusgrnumwwlk  28241  eupth2lems  28503  eupth2  28504  ipasslem1  29094  mdslmd1lem1  30588  mdslmd1lem2  30589  iuninc  30801  ssrelf  30856  nn0min  31036  gsumle  31252  gsumvsca1  31381  gsumvsca2  31382  ofldchr  31415  cmppcmp  31710  nexple  31877  esumfzf  31937  sseqp1  32262  rrvsum  32321  signstfvc  32453  bnj1174  32883  lfuhgr2  32980  subfacp1lem6  33047  mrsubvrs  33384  bccolsum  33611  iprodefisumlem  33612  faclimlem1  33615  ttrclss  33706  ttrclselem2  33712  naddssim  33764  nosupbnd1lem5  33842  noinfbnd1lem5  33857  onsuct0  34557  findfvcl  34568  poimirlem28  35732  sdclem2  35827  seqpo  35832  incsequz  35833  mettrifi  35842  heiborlem4  35899  bfplem1  35907  pclfinclN  37891  fzindd  39912  uzindd  39913  nnaddcom  40219  nnadddir  40221  nnmulcom  40223  sn-sup2  40360  incssnn0  40449  mzpexpmpt  40483  pell14qrexpclnn0  40604  monotuz  40679  rmxypos  40685  jm2.17a  40698  jm2.17b  40699  rmygeid  40702  jm2.18  40726  jm2.19lem3  40729  jm2.15nn0  40741  jm2.16nn0  40742  dfac11  40803  pwslnm  40835  hbtlem5  40869  cnsrexpcl  40906  relexpxpnnidm  41200  relexpiidm  41201  relexpss1d  41202  iunrelexpmin1  41205  relexpmulnn  41206  iunrelexpmin2  41209  relexp0a  41213  trclimalb2  41223  dvgrat  41819  lmodvsmdi  45606  tfis2d  46272