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  845  minimp  1619  cbv1v  2342  cbv1  2410  ralimdva  3173  reuss2  4345  ssrel  5806  ssrelOLD  5807  ssrel2  5809  ssrelrel  5820  funfvima2  7268  isofrlem  7376  dfwe2  7809  tfindsg  7898  tfinds2  7901  tfinds3  7902  trom  7912  findsg  7937  finds2  7938  xpord3inddlem  8195  fpr3g  8326  wfr3g  8363  tfrlem1  8432  tfr3  8455  tz7.48lem  8497  oaordi  8602  oeordi  8643  nnaordi  8674  nnawordi  8677  naddssim  8741  naddoa  8758  nneneq  9272  nneneqOLD  9284  ac6sfi  9348  fodomfi  9378  domunfican  9389  fodomfiOLD  9398  finsschain  9429  marypha1lem  9502  inf3lem2  9698  inf3lem5  9701  cantnfval2  9738  cantnflt  9741  cantnfp1lem3  9749  cnfcom  9769  ttrclss  9789  ttrclselem2  9795  frr3g  9825  dfac12lem3  10215  ackbij1lem16  10303  sornom  10346  infpssrlem4  10375  fin23lem34  10415  fin23lem36  10417  isf32lem1  10422  isf32lem2  10423  zorn2lem4  10568  zorn2lem5  10569  zorn2lem6  10570  zorn2lem7  10571  ttukeylem5  10582  pwfseqlem3  10729  wunfi  10790  grudomon  10886  prlem934  11102  sup2  12251  nnindd  12313  nnaddcl  12316  nnmulcl  12317  nnne0  12327  peano5uzi  12732  uzind2  12736  nn0indd  12740  fzind  12741  zindd  12744  fzindd  12745  uzaddcl  12969  uzwo  12976  om2uzlti  14001  seqcaopr3  14088  seqf1olem2a  14091  seqf1o  14094  ser1const  14109  expcllem  14123  expeq0  14143  mulexp  14152  expadd  14155  expmul  14158  expmordi  14217  leexp2r  14224  leexp1a  14225  bernneq  14278  modexp  14287  facdiv  14336  facwordi  14338  faclbnd  14339  faclbnd4lem4  14345  hashgadd  14426  hashmap  14484  hashf1lem2  14505  hashf1  14506  seqcoll  14513  cshweqrep  14869  relexpsucnnl  15079  relexpcnv  15084  relexpnndm  15090  relexpaddnn  15100  rlimsqzlem  15697  lo1le  15700  iseraltlem2  15731  fsum2d  15819  modfsummod  15842  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  binom  15878  climcndslem1  15897  climcndslem2  15898  cvgrat  15931  clim2prod  15936  prodfn0  15942  prodfrec  15943  ntrivcvgfvn0  15947  fprodabs  16022  fprod2d  16029  binomfallfac  16089  bpolycl  16100  fprodefsum  16143  demoivreALT  16249  ruclem8  16285  ruclem9  16286  dvdsfac  16374  bitsinv1  16488  sadcadd  16504  sadadd2  16506  saddisjlem  16510  smuval2  16528  smupvallem  16529  smu01lem  16531  smupval  16534  smueqlem  16536  smumullem  16538  rplpwr  16605  nn0seqcvgd  16617  seq1st  16618  alginv  16622  algcvga  16626  algfx  16627  prmdvdsexp  16762  prmfac1  16767  eulerthlem2  16829  pcmpt  16939  pcfac  16946  prmpwdvds  16951  prmreclem4  16966  vdwlem10  17037  ramcl  17076  mreexexd  17706  frmdgsum  18897  mulgnnass  19149  mhmmulg  19155  gsumwrev  19409  gsmsymgrfix  19470  gsmsymgreq  19474  efginvrel2  19769  efgsrel  19776  gsum2dlem2  20013  ablfac1eulem  20116  pgpfac  20128  srgmulgass  20244  srgpcomp  20245  srgbinom  20258  lmodvsmmulgdi  20917  cnfldexp  21440  assamulgscm  21944  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  mptcoe1fsupp  22238  coe1fzgsumdlem  22328  coe1fzgsumd  22329  gsummoncoe1  22333  evl1gsumdlem  22381  evl1gsumd  22382  mdetunilem9  22647  mptcoe1matfsupp  22829  mp2pm2mplem4  22836  chpdmat  22868  tgcl  22997  fiuncmp  23433  2ndcsep  23488  1stcelcls  23490  ptcmpfi  23842  tmdgsum  24124  fsumcn  24913  caubl  25361  caublcls  25362  ovolunlem1a  25550  ovolfiniun  25555  volfiniun  25601  voliunlem1  25604  volsuplem  25609  volsup  25610  dyadmax  25652  itgfsum  25882  dvnadd  25985  cpnord  25991  dvnfre  26010  dvmptfsum  26033  ply1divex  26196  fta1g  26229  plyco  26300  dgrcolem1  26333  dgrco  26335  dvnply2  26347  plydivex  26357  aaliou3lem2  26403  dvntaylp  26431  taylthlem1  26433  cxpmul2  26749  jensen  27050  ftalem2  27135  bcmono  27339  bposlem5  27350  lgsquad2lem2  27447  dchrisumlem1  27551  dchrisum0flb  27572  pntpbnd1  27648  pntlemf  27667  qabvle  27687  qabvexp  27688  ostthlem2  27690  ostth2lem2  27696  nosupbnd1lem5  27775  noinfbnd1lem5  27790  precsexlem8  28256  precsexlem9  28257  om2noseqrdg  28328  n0addscl  28365  n0mulscl  28366  peano5uzs  28408  expscl  28431  expsne0  28432  expsgt0  28433  pw2cut  28438  rusgrnumwwlk  30008  eupth2lems  30270  eupth2  30271  ipasslem1  30863  mdslmd1lem1  32357  mdslmd1lem2  32358  iuninc  32583  ssrelf  32637  nn0min  32824  gsumle  33074  gsumvsca1  33205  gsumvsca2  33206  domnprodn0  33247  ofldchr  33309  unitprodclb  33382  1arithufdlem3  33539  cmppcmp  33804  nexple  33973  esumfzf  34033  sseqp1  34360  rrvsum  34419  signstfvc  34551  bnj1174  34979  lfuhgr2  35086  subfacp1lem6  35153  mrsubvrs  35490  bccolsum  35701  iprodefisumlem  35702  faclimlem1  35705  onsuct0  36407  findfvcl  36418  poimirlem28  37608  sdclem2  37702  seqpo  37707  incsequz  37708  mettrifi  37717  heiborlem4  37774  bfplem1  37782  pclfinclN  39907  uzindd  41933  indstrd  42150  nnaddcom  42257  nnadddir  42259  nnmulcom  42261  sn-sup2  42447  incssnn0  42667  mzpexpmpt  42701  pell14qrexpclnn0  42822  monotuz  42898  rmxypos  42904  jm2.17a  42917  jm2.17b  42918  rmygeid  42921  jm2.18  42945  jm2.19lem3  42948  jm2.15nn0  42960  jm2.16nn0  42961  dfac11  43019  pwslnm  43051  hbtlem5  43085  cnsrexpcl  43122  cantnfresb  43286  onmcl  43293  naddonnn  43357  relexpxpnnidm  43665  relexpiidm  43666  relexpss1d  43667  iunrelexpmin1  43670  relexpmulnn  43671  iunrelexpmin2  43674  relexp0a  43678  trclimalb2  43688  dvgrat  44281  lmodvsmdi  48107  tfis2d  48772