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

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  44  imim2d  58  imim3i  65  loowoz  113  animpimp2impd  859  minimp  1651  cbv1v  2368  cbv1  2434  ralimdva  3177  reuss2  4280  ssrel  5771  ssrel2  5773  ssrelrel  5784  funfvima2  7231  isofrlem  7340  dfwe2  7774  tfindsg  7858  tfinds2  7861  tfinds3  7862  trom  7872  findsg  7895  finds2  7896  xpord3inddlem  8151  fpr3g  8283  wfr3g  8317  tfrlem1  8363  tfr3  8387  tz7.48lem  8429  oaordi  8532  oeordi  8574  nnaordi  8605  nnawordi  8608  naddssim  8673  naddoa  8690  nneneq  9191  ac6sfi  9245  fodomfi  9273  domunfican  9282  finsschain  9317  marypha1lem  9394  inf3lem2  9599  inf3lem5  9602  cantnfval2  9639  cantnflt  9642  cantnfp1lem3  9650  cnfcom  9670  ttrclss  9690  ttrclselem2  9696  frr3g  9729  dfac12lem3  10130  ackbij1lem16  10218  sornom  10262  infpssrlem4  10291  fin23lem34  10331  fin23lem36  10333  isf32lem1  10338  isf32lem2  10339  zorn2lem4  10484  zorn2lem5  10485  zorn2lem6  10486  zorn2lem7  10487  ttukeylem5  10498  pwfseqlem3  10646  wunfi  10707  grudomon  10803  prlem934  11019  sup2  12172  nnindd  12254  nnaddcl  12257  nnmulcl  12258  nnaddcom  12261  nnne0  12271  nnadddir  12293  nnmulcom  12295  peano5uzi  12686  uzind2  12690  nn0indd  12694  fzind  12695  zindd  12698  fzindd  12699  uzaddcl  12929  uzwo  12936  om2uzlti  13988  seqcaopr3  14075  seqf1olem2a  14078  seqf1o  14081  ser1const  14096  expcllem  14110  expeq0  14130  mulexp  14139  expadd  14142  expmul  14145  expmordi  14205  leexp2r  14212  leexp1a  14213  bernneq  14267  modexp  14276  facdiv  14325  facwordi  14327  faclbnd  14328  faclbnd4lem4  14334  hashgadd  14415  hashmap  14474  hashf1lem2  14495  hashf1  14496  seqcoll  14503  cshweqrep  14860  relexpsucnnl  15069  relexpcnv  15074  relexpnndm  15080  relexpaddnn  15090  rlimsqzlem  15702  lo1le  15705  iseraltlem2  15736  fsum2d  15824  modfsummod  15848  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  binom  15886  climcndslem1  15905  climcndslem2  15906  cvgrat  15939  clim2prod  15944  prodfn0  15950  prodfrec  15951  ntrivcvgfvn0  15955  fprodabs  16030  fprod2d  16037  binomfallfac  16096  bpolycl  16107  fprodefsum  16150  demoivreALT  16258  ruclem8  16294  ruclem9  16295  dvdsfac  16385  bitsinv1  16501  sadcadd  16517  sadadd2  16519  saddisjlem  16523  smuval2  16541  smupvallem  16542  smu01lem  16544  smupval  16547  smueqlem  16549  smumullem  16551  rplpwr  16617  nn0seqcvgd  16629  seq1st  16630  alginv  16634  algcvga  16638  algfx  16639  prmdvdsexp  16775  prmfac1  16780  eulerthlem2  16842  pcmpt  16953  pcfac  16960  prmpwdvds  16965  prmreclem4  16980  vdwlem10  17051  ramcl  17090  mreexexd  17705  frmdgsum  18922  mulgnnass  19176  mhmmulg  19182  gsumwrev  19437  gsmsymgrfix  19499  gsmsymgreq  19503  efginvrel2  19798  efgsrel  19805  gsum2dlem2  20042  ablfac1eulem  20145  pgpfac  20157  gsumle  20216  srgmulgass  20300  srgpcomp  20301  srgbinom  20314  lmodvsmmulgdi  20999  cnfldexp  21536  ofldchr  21707  assamulgscm  22032  mplcoe1  22169  mplcoe3  22170  mplcoe5  22172  mptcoe1fsupp  22356  coe1fzgsumdlem  22444  coe1fzgsumd  22445  gsummoncoe1  22449  evl1gsumdlem  22497  evl1gsumd  22498  mdetunilem9  22758  mptcoe1matfsupp  22940  mp2pm2mplem4  22947  chpdmat  22979  tgcl  23107  fiuncmp  23542  2ndcsep  23597  1stcelcls  23599  ptcmpfi  23951  tmdgsum  24233  fsumcn  25010  caubl  25448  caublcls  25449  ovolunlem1a  25636  ovolfiniun  25641  volfiniun  25687  voliunlem1  25690  volsuplem  25695  volsup  25696  dyadmax  25738  itgfsum  25967  dvnadd  26069  cpnord  26075  dvnfre  26092  dvmptfsum  26115  ply1divex  26275  fta1g  26308  plyco  26379  dgrcolem1  26411  dgrco  26413  dvnply2  26429  plydivex  26439  aaliou3lem2  26485  dvntaylp  26512  taylthlem1  26514  cxpmul2  26832  jensen  27131  ftalem2  27216  bcmono  27419  bposlem5  27430  lgsquad2lem2  27527  dchrisumlem1  27631  dchrisum0flb  27652  pntpbnd1  27728  pntlemf  27747  qabvle  27767  qabvexp  27768  ostthlem2  27770  ostth2lem2  27776  nosupbnd1lem5  27854  noinfbnd1lem5  27869  precsexlem8  28385  precsexlem9  28386  om2noseqrdg  28475  n0addscl  28515  n0mulscl  28516  eucliddivs  28547  peano5uzs  28575  expscllem  28601  expadds  28606  expsne0  28607  expsgt0  28608  pw2cut  28631  pw2cut2  28633  plngrotlem2  29048  rusgrnumwwlk  30305  eupth2lems  30567  eupth2  30568  ipasslem1  31161  mdslmd1lem1  32655  mdslmd1lem2  32656  iuninc  32883  ssrelf  32938  nn0min  33143  nexple  33155  gsumwun  33374  gsumvsca1  33524  gsumvsca2  33525  domnprodn0  33576  unitprodclb  33680  1arithufdlem3  33814  cmppcmp  34226  esumfzf  34437  sseqp1  34763  rrvsum  34822  signstfvc  34939  bnj1174  35369  lfuhgr2  35589  subfacp1lem6  35655  mrsubvrs  35992  bccolsum  36209  iprodefisumlem  36210  faclimlem1  36213  onsuct0  36930  findfvcl  36941  poimirlem28  38277  sdclem2  38371  seqpo  38376  incsequz  38377  mettrifi  38386  heiborlem4  38443  bfplem1  38451  pclfinclN  40702  uzindd  42723  indstrd  42938  sn-sup2  43243  incssnn0  43422  mzpexpmpt  43456  pell14qrexpclnn0  43573  monotuz  43648  rmxypos  43654  jm2.17a  43667  jm2.17b  43668  rmygeid  43671  jm2.18  43695  jm2.19lem3  43698  jm2.15nn0  43710  jm2.16nn0  43711  dfac11  43769  pwslnm  43801  hbtlem5  43835  cnsrexpcl  43872  cantnfresb  44031  onmcl  44038  naddonnn  44102  relexpxpnnidm  44409  relexpiidm  44410  relexpss1d  44411  iunrelexpmin1  44414  relexpmulnn  44415  iunrelexpmin2  44418  relexp0a  44422  trclimalb2  44432  dvgrat  45002  relpfrlem  45642  trfr  45651  lmodvsmdi  49136  tfis2d  50435