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  841  minimp  1603  cbv1v  2318  cbv1  2378  ralimdva  3144  reuss2  4203  ssrel  5543  ssrel2  5545  ssrelrel  5555  funfvima2  6859  isofrlem  6956  dfwe2  7352  tfindsg  7431  tfinds2  7434  tfinds3  7435  ordom  7445  findsg  7465  finds2  7466  wfr3g  7804  tfrlem1  7864  tfr3  7887  tz7.48lem  7928  oaordi  8022  oeordi  8063  nnaordi  8094  nnawordi  8097  nneneq  8547  ac6sfi  8608  domunfican  8637  fodomfi  8643  finsschain  8677  marypha1lem  8743  inf3lem2  8938  inf3lem5  8941  cantnfval2  8978  cantnflt  8981  cantnfp1lem3  8989  cnfcom  9009  dfac12lem3  9417  ackbij1lem16  9503  sornom  9545  infpssrlem4  9574  fin23lem34  9614  fin23lem36  9616  isf32lem1  9621  isf32lem2  9622  zorn2lem4  9767  zorn2lem5  9768  zorn2lem6  9769  zorn2lem7  9770  ttukeylem5  9781  pwfseqlem3  9928  wunfi  9989  grudomon  10085  prlem934  10301  sup2  11445  nnaddcl  11508  nnmulcl  11509  nnne0  11519  peano5uzi  11920  uzind2  11924  nn0indd  11928  fzind  11929  zindd  11932  uzaddcl  12153  uzwo  12160  om2uzlti  13168  seqcaopr3  13255  seqf1olem2a  13258  seqf1o  13261  ser1const  13276  expcllem  13290  expeq0  13309  mulexp  13318  expadd  13321  expmul  13324  expmordi  13381  leexp2r  13388  leexp1a  13389  bernneq  13440  modexp  13449  facdiv  13497  facwordi  13499  faclbnd  13500  faclbnd4lem4  13506  hashgadd  13586  hashmap  13644  hashf1lem2  13662  hashf1  13663  seqcoll  13670  cshweqrep  14019  relexpsucnnl  14225  relexpcnv  14228  relexpnndm  14234  relexpaddnn  14244  rlimsqzlem  14839  lo1le  14842  iseraltlem2  14873  fsum2d  14959  modfsummod  14982  fsumabs  14989  fsumrlim  14999  fsumo1  15000  fsumiun  15009  binom  15018  climcndslem1  15037  climcndslem2  15038  cvgrat  15072  clim2prod  15077  prodfn0  15083  prodfrec  15084  ntrivcvgfvn0  15088  fprodabs  15161  fprod2d  15168  binomfallfac  15228  bpolycl  15239  fprodefsum  15281  demoivreALT  15387  ruclem8  15423  ruclem9  15424  dvdsfac  15509  bitsinv1  15624  sadcadd  15640  sadadd2  15642  saddisjlem  15646  smuval2  15664  smupvallem  15665  smu01lem  15667  smupval  15670  smueqlem  15672  smumullem  15674  gcdmultiple  15729  rplpwr  15736  nn0seqcvgd  15743  seq1st  15744  alginv  15748  algcvga  15752  algfx  15753  prmdvdsexp  15888  prmfac1  15892  eulerthlem2  15948  pcmpt  16057  pcfac  16064  prmpwdvds  16069  prmreclem4  16084  vdwlem10  16155  ramcl  16194  mreexexd  16748  frmdgsum  17838  mulgnnass  18016  mhmmulg  18022  gsumwrev  18235  gsmsymgrfix  18287  gsmsymgreq  18291  efginvrel2  18580  efgsrel  18587  gsum2dlem2  18811  ablfac1eulem  18911  pgpfac  18923  srgmulgass  18971  srgpcomp  18972  srgbinom  18985  lmodvsmmulgdi  19359  assamulgscm  19818  mplcoe1  19933  mplcoe3  19934  mplcoe5  19936  mptcoe1fsupp  20066  coe1fzgsumdlem  20152  coe1fzgsumd  20153  gsummoncoe1  20155  evl1gsumdlem  20201  evl1gsumd  20202  cnfldexp  20260  mdetunilem9  20913  mptcoe1matfsupp  21094  mp2pm2mplem4  21101  chpdmat  21133  tgcl  21261  fiuncmp  21696  2ndcsep  21751  1stcelcls  21753  ptcmpfi  22105  tmdgsum  22387  fsumcn  23161  caubl  23594  caublcls  23595  ovolunlem1a  23780  ovolfiniun  23785  volfiniun  23831  voliunlem1  23834  volsuplem  23839  volsup  23840  dyadmax  23882  itgfsum  24110  dvnadd  24209  cpnord  24215  dvnfre  24232  dvmptfsum  24255  ply1divex  24413  fta1g  24444  plyco  24514  dgrcolem1  24546  dgrco  24548  dvnply2  24559  plydivex  24569  aaliou3lem2  24615  dvntaylp  24642  taylthlem1  24644  cxpmul2  24953  jensen  25248  ftalem2  25333  bcmono  25535  bposlem5  25546  lgsquad2lem2  25643  dchrisumlem1  25747  dchrisum0flb  25768  pntpbnd1  25844  pntlemf  25863  qabvle  25883  qabvexp  25884  ostthlem2  25886  ostth2lem2  25892  rusgrnumwwlk  27441  eupth2lems  27705  eupth2  27706  ipasslem1  28299  mdslmd1lem1  29793  mdslmd1lem2  29794  iuninc  30002  ssrelf  30056  nnindd  30220  nn0min  30221  gsumle  30494  gsumvsca1  30497  gsumvsca2  30498  ofldchr  30541  cmppcmp  30739  nexple  30885  esumfzf  30945  sseqp1  31270  rrvsum  31329  signstfvc  31461  bnj1174  31889  lfuhgr2  31977  subfacp1lem6  32040  mrsubvrs  32377  bccolsum  32579  iprodefisumlem  32580  faclimlem1  32583  trpredmintr  32679  frr3g  32730  fpr3g  32731  nosupbnd1lem5  32821  onsuct0  33398  findfvcl  33409  poimirlem28  34451  sdclem2  34549  seqpo  34554  incsequz  34555  mettrifi  34564  heiborlem4  34624  bfplem1  34632  pclfinclN  36617  nnaddcom  38686  incssnn0  38793  mzpexpmpt  38827  pell14qrexpclnn0  38948  monotuz  39023  rmxypos  39029  jm2.17a  39042  jm2.17b  39043  rmygeid  39046  jm2.18  39070  jm2.19lem3  39073  jm2.15nn0  39085  jm2.16nn0  39086  dfac11  39147  pwslnm  39179  hbtlem5  39213  cnsrexpcl  39250  relexpxpnnidm  39533  relexpiidm  39534  relexpss1d  39535  iunrelexpmin1  39538  relexpmulnn  39539  iunrelexpmin2  39542  relexp0a  39546  trclimalb2  39556  dvgrat  40182  lmodvsmdi  43910  tfis2d  44263