Theorem a2d 30

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 18	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpdd  44  imim2d  58  imim3i  65  loowoz  113  animpimp2impd  860  minimp  1654  cbv1v  2367  cbv1  2433  ralimdva  3176  reuss2  4275  ssrel  5767  ssrel2  5769  ssrelrel  5780  funfvima2  7234  isofrlem  7345  dfwe2  7777  tfindsg  7861  tfinds2  7864  tfinds3  7865  trom  7875  findsg  7898  finds2  7899  xpord3inddlem  8156  fpr3g  8288  wfr3g  8322  tfrlem1  8368  tfr3  8392  tz7.48lem  8434  oaordi  8537  oeordi  8579  nnaordi  8610  nnawordi  8613  naddssim  8678  naddoa  8695  nneneq  9204  ac6sfi  9258  fodomfi  9286  domunfican  9295  finsschain  9330  marypha1lem  9407  inf3lem2  9612  inf3lem5  9615  cantnfval2  9652  cantnflt  9655  cantnfp1lem3  9663  cnfcom  9683  ttrclss  9703  ttrclselem2  9709  frr3g  9742  dfac12lem3  10152  ackbij1lem16  10240  sornom  10283  infpssrlem4  10312  fin23lem34  10352  fin23lem36  10354  isf32lem1  10359  isf32lem2  10360  zorn2lem4  10505  zorn2lem5  10506  zorn2lem6  10507  zorn2lem7  10508  ttukeylem5  10519  pwfseqlem3  10673  wunfi  10734  grudomon  10830  prlem934  11046  sup2  12199  nnindd  12281  nnaddcl  12284  nnmulcl  12285  nnaddcom  12288  nnne0  12298  nnadddir  12320  nnmulcom  12322  peano5uzi  12714  uzind2  12718  nn0indd  12722  fzind  12723  zindd  12726  fzindd  12727  uzaddcl  12957  uzwo  12964  om2uzlti  14018  seqcaopr3  14105  seqf1olem2a  14108  seqf1o  14111  ser1const  14126  expcllem  14140  expeq0  14160  mulexp  14169  expadd  14172  expmul  14175  expmordi  14235  leexp2r  14242  leexp1a  14243  bernneq  14297  modexp  14306  facdiv  14355  facwordi  14357  faclbnd  14358  faclbnd4lem4  14364  hashgadd  14445  hashmap  14504  hashf1lem2  14525  hashf1  14526  seqcoll  14533  cshweqrep  14896  relexpsucnnl  15107  relexpcnv  15112  relexpnndm  15118  relexpaddnn  15128  rlimsqzlem  15740  lo1le  15743  iseraltlem2  15774  fsum2d  15861  modfsummod  15885  fsumabs  15892  fsumrlim  15902  fsumo1  15903  fsumiun  15912  binom  15923  climcndslem1  15942  climcndslem2  15943  cvgrat  15976  clim2prod  15981  prodfn0  15987  prodfrec  15988  ntrivcvgfvn0  15992  fprodabs  16067  fprod2d  16074  binomfallfac  16133  bpolycl  16144  fprodefsum  16187  demoivreALT  16295  ruclem8  16331  ruclem9  16332  dvdsfac  16422  bitsinv1  16538  sadcadd  16554  sadadd2  16556  saddisjlem  16560  smuval2  16578  smupvallem  16579  smu01lem  16581  smupval  16584  smueqlem  16586  smumullem  16588  rplpwr  16654  nn0seqcvgd  16666  seq1st  16667  alginv  16671  algcvga  16675  algfx  16676  prmdvdsexp  16812  prmfac1  16817  eulerthlem2  16879  pcmpt  16990  pcfac  16997  prmpwdvds  17002  prmreclem4  17017  vdwlem10  17088  ramcl  17127  mreexexd  17742  frmdgsum  18977  mulgnnass  19238  mhmmulg  19244  gsumwrev  19499  gsmsymgrfix  19561  gsmsymgreq  19565  efginvrel2  19860  efgsrel  19867  gsum2dlem2  20104  ablfac1eulem  20207  pgpfac  20219  gsumle  20278  srgmulgass  20362  srgpcomp  20363  srgbinom  20376  lmodvsmmulgdi  21087  cnfldexp  21624  ofldchr  21795  assamulgscm  22122  mplcoe1  22259  mplcoe3  22260  mplcoe5  22262  mptcoe1fsupp  22446  coe1fzgsumdlem  22534  coe1fzgsumd  22535  gsummoncoe1  22539  evl1gsumdlem  22587  evl1gsumd  22588  mdetunilem9  22848  mptcoe1matfsupp  23033  mp2pm2mplem4  23040  chpdmat  23072  tgcl  23200  fiuncmp  23635  2ndcsep  23691  1stcelcls  23693  ptcmpfi  24045  tmdgsum  24327  fsumcn  25104  caubl  25542  caublcls  25543  ovolunlem1a  25730  ovolfiniun  25735  volfiniun  25781  voliunlem1  25784  volsuplem  25789  volsup  25790  dyadmax  25832  itgfsum  26061  dvnadd  26163  cpnord  26169  dvnfre  26186  dvmptfsum  26209  ply1divex  26369  fta1g  26402  plyco  26474  dgrcolem1  26506  dgrco  26508  dvnply2  26524  plydivex  26534  aaliou3lem2  26586  dvntaylp  26614  taylthlem1  26616  cxpmul2  26934  jensen  27233  ftalem2  27318  bcmono  27521  bposlem5  27532  lgsquad2lem2  27629  dchrisumlem1  27733  dchrisum0flb  27754  pntpbnd1  27830  pntlemf  27849  qabvle  27869  qabvexp  27870  ostthlem2  27872  ostth2lem2  27878  nosupbnd1lem5  27956  noinfbnd1lem5  27971  precsexlem8  28487  precsexlem9  28488  om2noseqrdg  28577  n0addscl  28617  n0mulscl  28618  eucliddivs  28649  peano5uzs  28677  expscllem  28703  expadds  28708  expsne0  28709  expsgt0  28710  pw2cut  28733  pw2cut2  28735  plngrotlem2  29153  lfuhgr2  29614  rusgrnumwwlk  30454  eupth2lems  30726  eupth2  30727  ipasslem1  31320  mdslmd1lem1  32814  mdslmd1lem2  32815  iuninc  33042  ssrelf  33096  nn0min  33299  nexple  33311  gsumwun  33524  gsumvsca1  33674  gsumvsca2  33675  domnprodn0  33726  unitprodclb  33830  1arithufdlem3  33964  cmppcmp  34376  esumfzf  34587  sseqp1  34914  rrvsum  34973  signstfvc  35090  bnj1174  35520  subfacp1lem6  35772  mrsubvrs  36109  bccolsum  36326  iprodefisumlem  36327  faclimlem1  36330  onsuct0  37068  findfvcl  37079  poimirlem28  38405  sdclem2  38500  seqpo  38505  incsequz  38506  mettrifi  38515  heiborlem4  38572  bfplem1  38580  pclfinclN  40831  uzindd  42852  indstrd  43067  sn-sup2  43387  incssnn0  43564  mzpexpmpt  43598  pell14qrexpclnn0  43715  monotuz  43790  rmxypos  43796  jm2.17a  43809  jm2.17b  43810  rmygeid  43813  jm2.18  43837  jm2.19lem3  43840  jm2.15nn0  43852  jm2.16nn0  43853  dfac11  43911  pwslnm  43943  hbtlem5  43977  cnsrexpcl  44014  cantnfresb  44173  onmcl  44180  naddonnn  44244  relexpxpnnidm  44551  relexpiidm  44552  relexpss1d  44553  iunrelexpmin1  44556  relexpmulnn  44557  iunrelexpmin2  44560  relexp0a  44564  trclimalb2  44574  dvgrat  45144  relpfrlem  45784  trfr  45793  lmodvsmdi  49317  tfis2d  50614