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  2371  cbv1  2437  ralimdva  3180  reuss2  4282  ssrel  5774  ssrel2  5776  ssrelrel  5787  funfvima2  7236  isofrlem  7349  dfwe2  7782  tfindsg  7866  tfinds2  7869  tfinds3  7870  trom  7880  findsg  7903  finds2  7904  xpord3inddlem  8159  fpr3g  8291  wfr3g  8325  tfrlem1  8371  tfr3  8395  tz7.48lem  8437  oaordi  8540  oeordi  8582  nnaordi  8613  nnawordi  8616  naddssim  8681  naddoa  8698  nneneq  9200  ac6sfi  9254  fodomfi  9282  domunfican  9291  finsschain  9326  marypha1lem  9403  inf3lem2  9608  inf3lem5  9611  cantnfval2  9648  cantnflt  9651  cantnfp1lem3  9659  cnfcom  9679  ttrclss  9699  ttrclselem2  9705  frr3g  9738  dfac12lem3  10148  ackbij1lem16  10236  sornom  10279  infpssrlem4  10308  fin23lem34  10348  fin23lem36  10350  isf32lem1  10355  isf32lem2  10356  zorn2lem4  10501  zorn2lem5  10502  zorn2lem6  10503  zorn2lem7  10504  ttukeylem5  10515  pwfseqlem3  10663  wunfi  10724  grudomon  10820  prlem934  11036  sup2  12189  nnindd  12271  nnaddcl  12274  nnmulcl  12275  nnaddcom  12278  nnne0  12288  nnadddir  12310  nnmulcom  12312  peano5uzi  12703  uzind2  12707  nn0indd  12711  fzind  12712  zindd  12715  fzindd  12716  uzaddcl  12946  uzwo  12953  om2uzlti  14006  seqcaopr3  14093  seqf1olem2a  14096  seqf1o  14099  ser1const  14114  expcllem  14128  expeq0  14148  mulexp  14157  expadd  14160  expmul  14163  expmordi  14223  leexp2r  14230  leexp1a  14231  bernneq  14285  modexp  14294  facdiv  14343  facwordi  14345  faclbnd  14346  faclbnd4lem4  14352  hashgadd  14433  hashmap  14492  hashf1lem2  14513  hashf1  14514  seqcoll  14521  cshweqrep  14884  relexpsucnnl  15093  relexpcnv  15098  relexpnndm  15104  relexpaddnn  15114  rlimsqzlem  15726  lo1le  15729  iseraltlem2  15760  fsum2d  15848  modfsummod  15872  fsumabs  15879  fsumrlim  15889  fsumo1  15890  fsumiun  15899  binom  15910  climcndslem1  15929  climcndslem2  15930  cvgrat  15963  clim2prod  15968  prodfn0  15974  prodfrec  15975  ntrivcvgfvn0  15979  fprodabs  16054  fprod2d  16061  binomfallfac  16120  bpolycl  16131  fprodefsum  16174  demoivreALT  16282  ruclem8  16318  ruclem9  16319  dvdsfac  16409  bitsinv1  16525  sadcadd  16541  sadadd2  16543  saddisjlem  16547  smuval2  16565  smupvallem  16566  smu01lem  16568  smupval  16571  smueqlem  16573  smumullem  16575  rplpwr  16641  nn0seqcvgd  16653  seq1st  16654  alginv  16658  algcvga  16662  algfx  16663  prmdvdsexp  16799  prmfac1  16804  eulerthlem2  16866  pcmpt  16977  pcfac  16984  prmpwdvds  16989  prmreclem4  17004  vdwlem10  17075  ramcl  17114  mreexexd  17729  frmdgsum  18952  mulgnnass  19206  mhmmulg  19212  gsumwrev  19467  gsmsymgrfix  19529  gsmsymgreq  19533  efginvrel2  19828  efgsrel  19835  gsum2dlem2  20072  ablfac1eulem  20175  pgpfac  20187  gsumle  20246  srgmulgass  20330  srgpcomp  20331  srgbinom  20344  lmodvsmmulgdi  21055  cnfldexp  21592  ofldchr  21763  assamulgscm  22088  mplcoe1  22225  mplcoe3  22226  mplcoe5  22228  mptcoe1fsupp  22412  coe1fzgsumdlem  22500  coe1fzgsumd  22501  gsummoncoe1  22505  evl1gsumdlem  22553  evl1gsumd  22554  mdetunilem9  22814  mptcoe1matfsupp  22996  mp2pm2mplem4  23003  chpdmat  23035  tgcl  23163  fiuncmp  23598  2ndcsep  23653  1stcelcls  23655  ptcmpfi  24007  tmdgsum  24289  fsumcn  25066  caubl  25504  caublcls  25505  ovolunlem1a  25692  ovolfiniun  25697  volfiniun  25743  voliunlem1  25746  volsuplem  25751  volsup  25752  dyadmax  25794  itgfsum  26023  dvnadd  26125  cpnord  26131  dvnfre  26148  dvmptfsum  26171  ply1divex  26331  fta1g  26364  plyco  26435  dgrcolem1  26467  dgrco  26469  dvnply2  26485  plydivex  26495  aaliou3lem2  26543  dvntaylp  26571  taylthlem1  26573  cxpmul2  26891  jensen  27190  ftalem2  27275  bcmono  27478  bposlem5  27489  lgsquad2lem2  27586  dchrisumlem1  27690  dchrisum0flb  27711  pntpbnd1  27787  pntlemf  27806  qabvle  27826  qabvexp  27827  ostthlem2  27829  ostth2lem2  27835  nosupbnd1lem5  27913  noinfbnd1lem5  27928  precsexlem8  28444  precsexlem9  28445  om2noseqrdg  28534  n0addscl  28574  n0mulscl  28575  eucliddivs  28606  peano5uzs  28634  expscllem  28660  expadds  28665  expsne0  28666  expsgt0  28667  pw2cut  28690  pw2cut2  28692  plngrotlem2  29107  rusgrnumwwlk  30364  eupth2lems  30626  eupth2  30627  ipasslem1  31220  mdslmd1lem1  32714  mdslmd1lem2  32715  iuninc  32942  ssrelf  32997  nn0min  33202  nexple  33214  gsumwun  33427  gsumvsca1  33577  gsumvsca2  33578  domnprodn0  33629  unitprodclb  33733  1arithufdlem3  33867  cmppcmp  34279  esumfzf  34490  sseqp1  34816  rrvsum  34875  signstfvc  34992  bnj1174  35422  lfuhgr2  35631  subfacp1lem6  35697  mrsubvrs  36034  bccolsum  36251  iprodefisumlem  36252  faclimlem1  36255  onsuct0  36992  findfvcl  37003  poimirlem28  38339  sdclem2  38433  seqpo  38438  incsequz  38439  mettrifi  38448  heiborlem4  38505  bfplem1  38513  pclfinclN  40764  uzindd  42785  indstrd  43000  sn-sup2  43305  incssnn0  43482  mzpexpmpt  43516  pell14qrexpclnn0  43633  monotuz  43708  rmxypos  43714  jm2.17a  43727  jm2.17b  43728  rmygeid  43731  jm2.18  43755  jm2.19lem3  43758  jm2.15nn0  43770  jm2.16nn0  43771  dfac11  43829  pwslnm  43861  hbtlem5  43895  cnsrexpcl  43932  cantnfresb  44091  onmcl  44098  naddonnn  44162  relexpxpnnidm  44469  relexpiidm  44470  relexpss1d  44471  iunrelexpmin1  44474  relexpmulnn  44475  iunrelexpmin2  44478  relexp0a  44482  trclimalb2  44492  dvgrat  45062  relpfrlem  45702  trfr  45711  lmodvsmdi  49199  tfis2d  50498