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  852  minimp  1628  cbv1v  2344  cbv1  2410  ralimdva  3152  reuss2  4261  ssrel  5733  ssrel2  5735  ssrelrel  5746  funfvima2  7182  isofrlem  7291  dfwe2  7724  tfindsg  7808  tfinds2  7811  tfinds3  7812  trom  7822  findsg  7844  finds2  7845  xpord3inddlem  8101  fpr3g  8232  wfr3g  8266  tfrlem1  8312  tfr3  8335  tz7.48lem  8377  oaordi  8478  oeordi  8520  nnaordi  8551  nnawordi  8554  naddssim  8618  naddoa  8635  nneneq  9137  ac6sfi  9191  fodomfi  9219  domunfican  9229  fodomfiOLD  9237  finsschain  9266  marypha1lem  9343  inf3lem2  9548  inf3lem5  9551  cantnfval2  9588  cantnflt  9591  cantnfp1lem3  9599  cnfcom  9619  ttrclss  9639  ttrclselem2  9645  frr3g  9678  dfac12lem3  10066  ackbij1lem16  10154  sornom  10197  infpssrlem4  10226  fin23lem34  10266  fin23lem36  10268  isf32lem1  10273  isf32lem2  10274  zorn2lem4  10419  zorn2lem5  10420  zorn2lem6  10421  zorn2lem7  10422  ttukeylem5  10433  pwfseqlem3  10581  wunfi  10642  grudomon  10738  prlem934  10954  sup2  12110  nnindd  12192  nnaddcl  12195  nnmulcl  12196  nnaddcom  12199  nnne0  12209  nnadddir  12231  nnmulcom  12233  peano5uzi  12616  uzind2  12620  nn0indd  12624  fzind  12625  zindd  12628  fzindd  12629  uzaddcl  12852  uzwo  12859  om2uzlti  13910  seqcaopr3  13997  seqf1olem2a  14000  seqf1o  14003  ser1const  14018  expcllem  14032  expeq0  14052  mulexp  14061  expadd  14064  expmul  14067  expmordi  14127  leexp2r  14134  leexp1a  14135  bernneq  14189  modexp  14198  facdiv  14247  facwordi  14249  faclbnd  14250  faclbnd4lem4  14256  hashgadd  14337  hashmap  14395  hashf1lem2  14416  hashf1  14417  seqcoll  14424  cshweqrep  14781  relexpsucnnl  14990  relexpcnv  14995  relexpnndm  15001  relexpaddnn  15011  rlimsqzlem  15609  lo1le  15612  iseraltlem2  15643  fsum2d  15731  modfsummod  15755  fsumabs  15762  fsumrlim  15772  fsumo1  15773  fsumiun  15782  binom  15793  climcndslem1  15812  climcndslem2  15813  cvgrat  15846  clim2prod  15851  prodfn0  15857  prodfrec  15858  ntrivcvgfvn0  15862  fprodabs  15937  fprod2d  15944  binomfallfac  16004  bpolycl  16015  fprodefsum  16058  demoivreALT  16166  ruclem8  16202  ruclem9  16203  dvdsfac  16293  bitsinv1  16409  sadcadd  16425  sadadd2  16427  saddisjlem  16431  smuval2  16449  smupvallem  16450  smu01lem  16452  smupval  16455  smueqlem  16457  smumullem  16459  rplpwr  16525  nn0seqcvgd  16537  seq1st  16538  alginv  16542  algcvga  16546  algfx  16547  prmdvdsexp  16683  prmfac1  16688  eulerthlem2  16750  pcmpt  16861  pcfac  16868  prmpwdvds  16873  prmreclem4  16888  vdwlem10  16959  ramcl  16998  mreexexd  17612  frmdgsum  18828  mulgnnass  19083  mhmmulg  19089  gsumwrev  19339  gsmsymgrfix  19401  gsmsymgreq  19405  efginvrel2  19700  efgsrel  19707  gsum2dlem2  19944  ablfac1eulem  20047  pgpfac  20059  gsumle  20118  srgmulgass  20196  srgpcomp  20197  srgbinom  20210  lmodvsmmulgdi  20894  cnfldexp  21387  ofldchr  21558  assamulgscm  21883  mplcoe1  22020  mplcoe3  22021  mplcoe5  22023  mptcoe1fsupp  22207  coe1fzgsumdlem  22296  coe1fzgsumd  22297  gsummoncoe1  22301  evl1gsumdlem  22349  evl1gsumd  22350  mdetunilem9  22610  mptcoe1matfsupp  22792  mp2pm2mplem4  22799  chpdmat  22831  tgcl  22959  fiuncmp  23394  2ndcsep  23449  1stcelcls  23451  ptcmpfi  23803  tmdgsum  24085  fsumcn  24862  caubl  25300  caublcls  25301  ovolunlem1a  25488  ovolfiniun  25493  volfiniun  25539  voliunlem1  25542  volsuplem  25547  volsup  25548  dyadmax  25590  itgfsum  25819  dvnadd  25921  cpnord  25927  dvnfre  25944  dvmptfsum  25967  ply1divex  26127  fta1g  26160  plyco  26231  dgrcolem1  26263  dgrco  26265  dvnply2  26278  plydivex  26288  aaliou3lem2  26334  dvntaylp  26361  taylthlem1  26363  cxpmul2  26678  jensen  26977  ftalem2  27062  bcmono  27265  bposlem5  27276  lgsquad2lem2  27373  dchrisumlem1  27477  dchrisum0flb  27498  pntpbnd1  27574  pntlemf  27593  qabvle  27613  qabvexp  27614  ostthlem2  27616  ostth2lem2  27622  nosupbnd1lem5  27701  noinfbnd1lem5  27716  precsexlem8  28231  precsexlem9  28232  om2noseqrdg  28321  n0addscl  28361  n0mulscl  28362  eucliddivs  28393  peano5uzs  28421  expscllem  28447  expadds  28452  expsne0  28453  expsgt0  28454  pw2cut  28477  pw2cut2  28479  rusgrnumwwlk  30071  eupth2lems  30333  eupth2  30334  ipasslem1  30927  mdslmd1lem1  32421  mdslmd1lem2  32422  iuninc  32656  ssrelf  32714  nn0min  32920  nexple  32943  gsumwun  33164  gsumvsca1  33314  gsumvsca2  33315  domnprodn0  33363  unitprodclb  33479  1arithufdlem3  33636  cmppcmp  34049  esumfzf  34260  sseqp1  34586  rrvsum  34645  signstfvc  34765  bnj1174  35192  lfuhgr2  35354  subfacp1lem6  35420  mrsubvrs  35757  bccolsum  35974  iprodefisumlem  35975  faclimlem1  35978  onsuct0  36676  findfvcl  36687  poimirlem28  38022  sdclem2  38116  seqpo  38121  incsequz  38122  mettrifi  38131  heiborlem4  38188  bfplem1  38196  pclfinclN  40449  uzindd  42470  indstrd  42685  sn-sup2  42988  incssnn0  43167  mzpexpmpt  43201  pell14qrexpclnn0  43318  monotuz  43393  rmxypos  43399  jm2.17a  43412  jm2.17b  43413  rmygeid  43416  jm2.18  43440  jm2.19lem3  43443  jm2.15nn0  43455  jm2.16nn0  43456  dfac11  43514  pwslnm  43546  hbtlem5  43580  cnsrexpcl  43617  cantnfresb  43776  onmcl  43783  naddonnn  43847  relexpxpnnidm  44154  relexpiidm  44155  relexpss1d  44156  iunrelexpmin1  44159  relexpmulnn  44160  iunrelexpmin2  44163  relexp0a  44167  trclimalb2  44177  dvgrat  44763  relpfrlem  45404  trfr  45413  lmodvsmdi  48877  tfis2d  50177