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  2369  cbv1  2434  ralimdva  3178  reuss2  4274  ssrel  5764  ssrel2  5766  ssrelrel  5777  funfvima2  7260  isofrlem  7371  dfwe2  7812  tfindsg  7896  tfinds2  7899  tfinds3  7900  trom  7910  findsg  7933  finds2  7934  xpord3inddlem  8198  fpr3g  8331  wfr3g  8365  tfrlem1  8411  tfr3  8435  tz7.48lemOLD  8479  oaordi  8582  oeordi  8624  nnaordi  8655  nnawordi  8658  naddssim  8723  naddoa  8740  nneneq  9249  ac6sfi  9303  fodomfi  9332  domunfican  9341  finsschain  9376  marypha1lem  9452  inf3lem2  9657  inf3lem5  9660  cantnfval2  9697  cantnflt  9700  cantnfp1lem3  9708  cnfcom  9728  ttrclss  9748  ttrclselem2  9754  frr3g  9787  dfac12lem3  10251  ackbij1lem16  10339  sornom  10382  infpssrlem4  10411  fin23lem34  10451  fin23lem36  10453  isf32lem1  10458  isf32lem2  10459  zorn2lem4  10604  zorn2lem5  10605  zorn2lem6  10606  zorn2lem7  10607  ttukeylem5  10618  pwfseqlem3  10772  wunfi  10833  grudomon  10929  prlem934  11145  sup2  12300  nnindd  12382  nnaddcl  12385  nnmulcl  12386  nnaddcom  12389  nnne0  12399  nnadddir  12421  nnmulcom  12423  peano5uzi  12815  uzind2  12819  nn0indd  12823  fzind  12824  zindd  12827  fzindd  12828  uzaddcl  13058  uzwo  13065  om2uzlti  14120  seqcaopr3  14207  seqf1olem2a  14210  seqf1o  14213  ser1const  14228  expcllem  14242  expeq0  14262  mulexp  14271  expadd  14274  expmul  14277  expmordi  14337  leexp2r  14344  leexp1a  14345  bernneq  14400  modexp  14409  facdiv  14458  facwordi  14460  faclbnd  14461  faclbnd4lem4  14467  hashgadd  14548  hashmap  14607  hashf1lem2  14628  hashf1  14629  seqcoll  14636  cshweqrep  15000  relexpsucnnl  15212  relexpcnv  15217  relexpnndm  15223  relexpaddnn  15233  rlimsqzlem  15845  lo1le  15848  iseraltlem2  15879  fsum2d  15966  modfsummod  15990  fsumabs  15997  fsumrlim  16007  fsumo1  16008  fsumiun  16017  binom  16028  climcndslem1  16047  climcndslem2  16048  cvgrat  16081  clim2prod  16086  prodfn0  16092  prodfrec  16093  ntrivcvgfvn0  16097  fprodabs  16170  fprod2d  16177  binomfallfac  16236  bpolycl  16247  fprodefsum  16290  demoivreALT  16398  ruclem8  16434  ruclem9  16435  dvdsfac  16525  bitsinv1  16641  sadcadd  16657  sadadd2  16659  saddisjlem  16663  smuval2  16681  smupvallem  16682  smu01lem  16684  smupval  16687  smueqlem  16689  smumullem  16691  rplpwr  16761  nn0seqcvgd  16774  seq1st  16775  alginv  16779  algcvga  16783  algfx  16784  prmdvdsexp  16920  prmfac1  16925  eulerthlem2  16988  pcmpt  17099  pcfac  17106  prmpwdvds  17111  prmreclem4  17126  vdwlem10  17197  ramcl  17236  mreexexd  17851  frmdgsum  19087  mulgnnass  19348  mhmmulg  19354  gsumwrev  19610  gsmsymgrfix  19672  gsmsymgreq  19676  efginvrel2  19971  efgsrel  19978  gsum2dlem2  20215  ablfac1eulem  20318  pgpfac  20330  gsumle  20389  srgmulgass  20473  srgpcomp  20474  srgbinom  20487  lmodvsmmulgdi  21202  cnfldexp  21741  ofldchr  21912  assamulgscm  22239  mplcoe1  22376  mplcoe3  22377  mplcoe5  22379  mptcoe1fsupp  22563  coe1fzgsumdlem  22651  coe1fzgsumd  22652  gsummoncoe1  22656  evl1gsumdlem  22704  evl1gsumd  22705  mdetunilem9  22965  mptcoe1matfsupp  23150  mp2pm2mplem4  23157  chpdmat  23189  tgcl  23317  fiuncmp  23752  2ndcsep  23808  1stcelcls  23810  ptcmpfi  24162  tmdgsum  24444  fsumcn  25221  caubl  25659  caublcls  25660  ovolunlem1a  25847  ovolfiniun  25852  volfiniun  25898  voliunlem1  25901  volsuplem  25906  volsup  25907  dyadmax  25949  itgfsum  26177  dvnadd  26279  cpnord  26285  dvnfre  26302  dvmptfsum  26325  ply1divex  26485  fta1g  26518  plyco  26590  dgrcolem1  26622  dgrco  26624  dvnply2  26638  plydivex  26648  aaliou3lem2  26700  dvntaylp  26728  taylthlem1  26730  cxpmul2  27047  jensen  27346  ftalem2  27431  bcmono  27634  bposlem5  27645  lgsquad2lem2  27742  dchrisumlem1  27846  dchrisum0flb  27867  pntpbnd1  27943  pntlemf  27962  qabvle  27982  qabvexp  27983  ostthlem2  27985  ostth2lem2  27991  nosupbnd1lem5  28099  noinfbnd1lem5  28114  precsexlem8  28630  precsexlem9  28631  om2noseqrdg  28720  n0addscl  28760  n0mulscl  28761  eucliddivs  28792  peano5uzs  28820  expscllem  28846  expadds  28851  expsne0  28852  expsgt0  28853  pw2cut  28876  pw2cut2  28878  plngrotlem2  29296  lfuhgr2  29757  rusgrnumwwlk  30597  eupth2lems  30869  eupth2  30870  ipasslem1  31463  mdslmd1lem1  32957  mdslmd1lem2  32958  iuninc  33227  ssrelf  33281  nn0min  33482  nexple  33494  gsumwun  33707  gsumvsca1  33857  gsumvsca2  33858  domnprodn0  33909  unitprodclb  34014  1arithufdlem3  34148  cmppcmp  34560  esumfzf  34771  sseqp1  35097  rrvsum  35156  signstfvc  35273  bnj1174  35703  subfacp1lem6  36117  mrsubvrs  36454  bccolsum  36682  iprodefisumlem  36683  faclimlem1  36686  onsuct0  37407  findfvcl  37418  poimirlem28  38758  sdclem2  38868  seqpo  38873  incsequz  38874  mettrifi  38883  heiborlem4  38940  bfplem1  38948  pclfinclN  41199  uzindd  43220  indstrd  43435  sn-sup2  43748  incssnn0  43915  mzpexpmpt  43949  pell14qrexpclnn0  44066  monotuz  44141  rmxypos  44147  jm2.17a  44160  jm2.17b  44161  rmygeid  44164  jm2.18  44188  jm2.19lem3  44191  jm2.15nn0  44203  jm2.16nn0  44204  dfac11  44257  pwslnm  44289  hbtlem5  44322  cnsrexpcl  44359  cantnfresb  44518  onmcl  44525  naddonnn  44589  relexpxpnnidm  44895  relexpiidm  44896  relexpss1d  44897  iunrelexpmin1  44900  relexpmulnn  44901  iunrelexpmin2  44904  relexp0a  44908  trclimalb2  44918  dvgrat  45488  relpfrlem  46138  trfr  46147  lmodvsmdi  49696  tfis2d  51067