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  3141  reuss2  4279  ssrel  5730  ssrel2  5732  ssrelrel  5743  funfvima2  7171  isofrlem  7281  dfwe2  7714  tfindsg  7801  tfinds2  7804  tfinds3  7805  trom  7815  findsg  7837  finds2  7838  xpord3inddlem  8094  fpr3g  8225  wfr3g  8259  tfrlem1  8305  tfr3  8328  tz7.48lem  8370  oaordi  8471  oeordi  8512  nnaordi  8543  nnawordi  8546  naddssim  8610  naddoa  8627  nneneq  9130  ac6sfi  9189  fodomfi  9219  domunfican  9230  fodomfiOLD  9239  finsschain  9268  marypha1lem  9342  inf3lem2  9544  inf3lem5  9547  cantnfval2  9584  cantnflt  9587  cantnfp1lem3  9595  cnfcom  9615  ttrclss  9635  ttrclselem2  9641  frr3g  9671  dfac12lem3  10059  ackbij1lem16  10147  sornom  10190  infpssrlem4  10219  fin23lem34  10259  fin23lem36  10261  isf32lem1  10266  isf32lem2  10267  zorn2lem4  10412  zorn2lem5  10413  zorn2lem6  10414  zorn2lem7  10415  ttukeylem5  10426  pwfseqlem3  10573  wunfi  10634  grudomon  10730  prlem934  10946  sup2  12099  nnindd  12166  nnaddcl  12169  nnmulcl  12170  nnne0  12180  peano5uzi  12583  uzind2  12587  nn0indd  12591  fzind  12592  zindd  12595  fzindd  12596  uzaddcl  12823  uzwo  12830  om2uzlti  13875  seqcaopr3  13962  seqf1olem2a  13965  seqf1o  13968  ser1const  13983  expcllem  13997  expeq0  14017  mulexp  14026  expadd  14029  expmul  14032  expmordi  14092  leexp2r  14099  leexp1a  14100  bernneq  14154  modexp  14163  facdiv  14212  facwordi  14214  faclbnd  14215  faclbnd4lem4  14221  hashgadd  14302  hashmap  14360  hashf1lem2  14381  hashf1  14382  seqcoll  14389  cshweqrep  14745  relexpsucnnl  14955  relexpcnv  14960  relexpnndm  14966  relexpaddnn  14976  rlimsqzlem  15574  lo1le  15577  iseraltlem2  15608  fsum2d  15696  modfsummod  15719  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  binom  15755  climcndslem1  15774  climcndslem2  15775  cvgrat  15808  clim2prod  15813  prodfn0  15819  prodfrec  15820  ntrivcvgfvn0  15824  fprodabs  15899  fprod2d  15906  binomfallfac  15966  bpolycl  15977  fprodefsum  16020  demoivreALT  16128  ruclem8  16164  ruclem9  16165  dvdsfac  16255  bitsinv1  16371  sadcadd  16387  sadadd2  16389  saddisjlem  16393  smuval2  16411  smupvallem  16412  smu01lem  16414  smupval  16417  smueqlem  16419  smumullem  16421  rplpwr  16487  nn0seqcvgd  16499  seq1st  16500  alginv  16504  algcvga  16508  algfx  16509  prmdvdsexp  16644  prmfac1  16649  eulerthlem2  16711  pcmpt  16822  pcfac  16829  prmpwdvds  16834  prmreclem4  16849  vdwlem10  16920  ramcl  16959  mreexexd  17572  frmdgsum  18754  mulgnnass  19006  mhmmulg  19012  gsumwrev  19263  gsmsymgrfix  19325  gsmsymgreq  19329  efginvrel2  19624  efgsrel  19631  gsum2dlem2  19868  ablfac1eulem  19971  pgpfac  19983  gsumle  20042  srgmulgass  20120  srgpcomp  20121  srgbinom  20134  lmodvsmmulgdi  20818  cnfldexp  21329  ofldchr  21501  assamulgscm  21826  mplcoe1  21960  mplcoe3  21961  mplcoe5  21963  mptcoe1fsupp  22116  coe1fzgsumdlem  22206  coe1fzgsumd  22207  gsummoncoe1  22211  evl1gsumdlem  22259  evl1gsumd  22260  mdetunilem9  22523  mptcoe1matfsupp  22705  mp2pm2mplem4  22712  chpdmat  22744  tgcl  22872  fiuncmp  23307  2ndcsep  23362  1stcelcls  23364  ptcmpfi  23716  tmdgsum  23998  fsumcn  24777  caubl  25224  caublcls  25225  ovolunlem1a  25413  ovolfiniun  25418  volfiniun  25464  voliunlem1  25467  volsuplem  25472  volsup  25473  dyadmax  25515  itgfsum  25744  dvnadd  25847  cpnord  25853  dvnfre  25872  dvmptfsum  25895  ply1divex  26058  fta1g  26091  plyco  26162  dgrcolem1  26195  dgrco  26197  dvnply2  26211  plydivex  26221  aaliou3lem2  26267  dvntaylp  26295  taylthlem1  26297  cxpmul2  26614  jensen  26915  ftalem2  27000  bcmono  27204  bposlem5  27215  lgsquad2lem2  27312  dchrisumlem1  27416  dchrisum0flb  27437  pntpbnd1  27513  pntlemf  27532  qabvle  27552  qabvexp  27553  ostthlem2  27555  ostth2lem2  27561  nosupbnd1lem5  27640  noinfbnd1lem5  27655  precsexlem8  28139  precsexlem9  28140  om2noseqrdg  28221  n0addscl  28259  n0mulscl  28260  eucliddivs  28288  peano5uzs  28315  expscllem  28340  expadds  28345  expsne0  28346  expsgt0  28347  pw2cut  28366  rusgrnumwwlk  29938  eupth2lems  30200  eupth2  30201  ipasslem1  30793  mdslmd1lem1  32287  mdslmd1lem2  32288  iuninc  32522  ssrelf  32576  nn0min  32778  nexple  32802  gsumwun  33031  gsumvsca1  33178  gsumvsca2  33179  domnprodn0  33225  unitprodclb  33336  1arithufdlem3  33493  cmppcmp  33824  esumfzf  34035  sseqp1  34362  rrvsum  34421  signstfvc  34541  bnj1174  34969  lfuhgr2  35091  subfacp1lem6  35157  mrsubvrs  35494  bccolsum  35711  iprodefisumlem  35712  faclimlem1  35715  onsuct0  36414  findfvcl  36425  poimirlem28  37627  sdclem2  37721  seqpo  37726  incsequz  37727  mettrifi  37736  heiborlem4  37793  bfplem1  37801  pclfinclN  39929  uzindd  41950  indstrd  42166  nnaddcom  42241  nnadddir  42243  nnmulcom  42245  sn-sup2  42464  incssnn0  42684  mzpexpmpt  42718  pell14qrexpclnn0  42839  monotuz  42914  rmxypos  42920  jm2.17a  42933  jm2.17b  42934  rmygeid  42937  jm2.18  42961  jm2.19lem3  42964  jm2.15nn0  42976  jm2.16nn0  42977  dfac11  43035  pwslnm  43067  hbtlem5  43101  cnsrexpcl  43138  cantnfresb  43297  onmcl  43304  naddonnn  43368  relexpxpnnidm  43676  relexpiidm  43677  relexpss1d  43678  iunrelexpmin1  43681  relexpmulnn  43682  iunrelexpmin2  43685  relexp0a  43689  trclimalb2  43699  dvgrat  44285  relpfrlem  44927  trfr  44936  lmodvsmdi  48364  tfis2d  49666