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  844  minimp  1623  cbv1v  2332  cbv1  2401  ralimdva  3167  reuss2  4315  ssrel  5782  ssrelOLD  5783  ssrel2  5785  ssrelrel  5796  funfvima2  7235  isofrlem  7339  dfwe2  7763  tfindsg  7852  tfinds2  7855  tfinds3  7856  trom  7866  findsg  7892  finds2  7893  xpord3inddlem  8142  fpr3g  8272  wfr3g  8309  tfrlem1  8378  tfr3  8401  tz7.48lem  8443  oaordi  8548  oeordi  8589  nnaordi  8620  nnawordi  8623  naddssim  8686  nneneq  9211  nneneqOLD  9223  ac6sfi  9289  domunfican  9322  fodomfi  9327  finsschain  9361  marypha1lem  9430  inf3lem2  9626  inf3lem5  9629  cantnfval2  9666  cantnflt  9669  cantnfp1lem3  9677  cnfcom  9697  ttrclss  9717  ttrclselem2  9723  frr3g  9753  dfac12lem3  10142  ackbij1lem16  10232  sornom  10274  infpssrlem4  10303  fin23lem34  10343  fin23lem36  10345  isf32lem1  10350  isf32lem2  10351  zorn2lem4  10496  zorn2lem5  10497  zorn2lem6  10498  zorn2lem7  10499  ttukeylem5  10510  pwfseqlem3  10657  wunfi  10718  grudomon  10814  prlem934  11030  sup2  12172  nnindd  12234  nnaddcl  12237  nnmulcl  12238  nnne0  12248  peano5uzi  12653  uzind2  12657  nn0indd  12661  fzind  12662  zindd  12665  fzindd  12666  uzaddcl  12890  uzwo  12897  om2uzlti  13917  seqcaopr3  14005  seqf1olem2a  14008  seqf1o  14011  ser1const  14026  expcllem  14040  expeq0  14060  mulexp  14069  expadd  14072  expmul  14075  expmordi  14134  leexp2r  14141  leexp1a  14142  bernneq  14194  modexp  14203  facdiv  14249  facwordi  14251  faclbnd  14252  faclbnd4lem4  14258  hashgadd  14339  hashmap  14397  hashf1lem2  14419  hashf1  14420  seqcoll  14427  cshweqrep  14773  relexpsucnnl  14979  relexpcnv  14984  relexpnndm  14990  relexpaddnn  15000  rlimsqzlem  15597  lo1le  15600  iseraltlem2  15631  fsum2d  15719  modfsummod  15742  fsumabs  15749  fsumrlim  15759  fsumo1  15760  fsumiun  15769  binom  15778  climcndslem1  15797  climcndslem2  15798  cvgrat  15831  clim2prod  15836  prodfn0  15842  prodfrec  15843  ntrivcvgfvn0  15847  fprodabs  15920  fprod2d  15927  binomfallfac  15987  bpolycl  15998  fprodefsum  16040  demoivreALT  16146  ruclem8  16182  ruclem9  16183  dvdsfac  16271  bitsinv1  16385  sadcadd  16401  sadadd2  16403  saddisjlem  16407  smuval2  16425  smupvallem  16426  smu01lem  16428  smupval  16431  smueqlem  16433  smumullem  16435  rplpwr  16501  nn0seqcvgd  16509  seq1st  16510  alginv  16514  algcvga  16518  algfx  16519  prmdvdsexp  16654  prmfac1  16660  eulerthlem2  16717  pcmpt  16827  pcfac  16834  prmpwdvds  16839  prmreclem4  16854  vdwlem10  16925  ramcl  16964  mreexexd  17594  frmdgsum  18745  mulgnnass  18991  mhmmulg  18997  gsumwrev  19235  gsmsymgrfix  19298  gsmsymgreq  19302  efginvrel2  19597  efgsrel  19604  gsum2dlem2  19841  ablfac1eulem  19944  pgpfac  19956  srgmulgass  20042  srgpcomp  20043  srgbinom  20056  lmodvsmmulgdi  20512  cnfldexp  20984  assamulgscm  21461  mplcoe1  21598  mplcoe3  21599  mplcoe5  21601  mptcoe1fsupp  21745  coe1fzgsumdlem  21832  coe1fzgsumd  21833  gsummoncoe1  21835  evl1gsumdlem  21882  evl1gsumd  21883  mdetunilem9  22129  mptcoe1matfsupp  22311  mp2pm2mplem4  22318  chpdmat  22350  tgcl  22479  fiuncmp  22915  2ndcsep  22970  1stcelcls  22972  ptcmpfi  23324  tmdgsum  23606  fsumcn  24393  caubl  24832  caublcls  24833  ovolunlem1a  25020  ovolfiniun  25025  volfiniun  25071  voliunlem1  25074  volsuplem  25079  volsup  25080  dyadmax  25122  itgfsum  25351  dvnadd  25453  cpnord  25459  dvnfre  25476  dvmptfsum  25499  ply1divex  25661  fta1g  25692  plyco  25762  dgrcolem1  25794  dgrco  25796  dvnply2  25807  plydivex  25817  aaliou3lem2  25863  dvntaylp  25890  taylthlem1  25892  cxpmul2  26204  jensen  26500  ftalem2  26585  bcmono  26787  bposlem5  26798  lgsquad2lem2  26895  dchrisumlem1  26999  dchrisum0flb  27020  pntpbnd1  27096  pntlemf  27115  qabvle  27135  qabvexp  27136  ostthlem2  27138  ostth2lem2  27144  nosupbnd1lem5  27222  noinfbnd1lem5  27237  precsexlem8  27670  precsexlem9  27671  rusgrnumwwlk  29267  eupth2lems  29529  eupth2  29530  ipasslem1  30122  mdslmd1lem1  31616  mdslmd1lem2  31617  iuninc  31830  ssrelf  31882  nn0min  32064  gsumle  32283  gsumvsca1  32412  gsumvsca2  32413  ofldchr  32473  cmppcmp  32907  nexple  33076  esumfzf  33136  sseqp1  33463  rrvsum  33522  signstfvc  33654  bnj1174  34083  lfuhgr2  34178  subfacp1lem6  34245  mrsubvrs  34582  bccolsum  34784  iprodefisumlem  34785  faclimlem1  34788  onsuct0  35418  findfvcl  35429  poimirlem28  36608  sdclem2  36702  seqpo  36707  incsequz  36708  mettrifi  36717  heiborlem4  36774  bfplem1  36782  pclfinclN  38913  uzindd  40934  nnaddcom  41270  nnadddir  41272  nnmulcom  41274  sn-sup2  41430  incssnn0  41537  mzpexpmpt  41571  pell14qrexpclnn0  41692  monotuz  41768  rmxypos  41774  jm2.17a  41787  jm2.17b  41788  rmygeid  41791  jm2.18  41815  jm2.19lem3  41818  jm2.15nn0  41830  jm2.16nn0  41831  dfac11  41892  pwslnm  41924  hbtlem5  41958  cnsrexpcl  41995  cantnfresb  42162  onmcl  42169  naddonnn  42234  relexpxpnnidm  42542  relexpiidm  42543  relexpss1d  42544  iunrelexpmin1  42547  relexpmulnn  42548  iunrelexpmin2  42551  relexp0a  42555  trclimalb2  42565  dvgrat  43159  lmodvsmdi  47143  tfis2d  47809