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  857  minimp  1640  cbv1v  2366  cbv1  2432  ralimdva  3173  reuss2  4278  ssrel  5753  ssrel2  5755  ssrelrel  5766  funfvima2  7211  isofrlem  7320  dfwe2  7753  tfindsg  7837  tfinds2  7840  tfinds3  7841  trom  7851  findsg  7874  finds2  7875  xpord3inddlem  8129  fpr3g  8261  wfr3g  8295  tfrlem1  8341  tfr3  8365  tz7.48lem  8407  oaordi  8510  oeordi  8552  nnaordi  8583  nnawordi  8586  naddssim  8651  naddoa  8668  nneneq  9170  ac6sfi  9224  fodomfi  9252  domunfican  9262  fodomfiOLD  9270  finsschain  9299  marypha1lem  9376  inf3lem2  9581  inf3lem5  9584  cantnfval2  9621  cantnflt  9624  cantnfp1lem3  9632  cnfcom  9652  ttrclss  9672  ttrclselem2  9678  frr3g  9711  dfac12lem3  10099  ackbij1lem16  10187  sornom  10231  infpssrlem4  10260  fin23lem34  10300  fin23lem36  10302  isf32lem1  10307  isf32lem2  10308  zorn2lem4  10453  zorn2lem5  10454  zorn2lem6  10455  zorn2lem7  10456  ttukeylem5  10467  pwfseqlem3  10615  wunfi  10676  grudomon  10772  prlem934  10988  sup2  12145  nnindd  12227  nnaddcl  12230  nnmulcl  12231  nnaddcom  12234  nnne0  12244  nnadddir  12266  nnmulcom  12268  peano5uzi  12659  uzind2  12663  nn0indd  12667  fzind  12668  zindd  12671  fzindd  12672  uzaddcl  12902  uzwo  12909  om2uzlti  13960  seqcaopr3  14047  seqf1olem2a  14050  seqf1o  14053  ser1const  14068  expcllem  14082  expeq0  14102  mulexp  14111  expadd  14114  expmul  14117  expmordi  14177  leexp2r  14184  leexp1a  14185  bernneq  14239  modexp  14248  facdiv  14297  facwordi  14299  faclbnd  14300  faclbnd4lem4  14306  hashgadd  14387  hashmap  14445  hashf1lem2  14466  hashf1  14467  seqcoll  14474  cshweqrep  14831  relexpsucnnl  15040  relexpcnv  15045  relexpnndm  15051  relexpaddnn  15061  rlimsqzlem  15659  lo1le  15662  iseraltlem2  15693  fsum2d  15781  modfsummod  15805  fsumabs  15812  fsumrlim  15822  fsumo1  15823  fsumiun  15832  binom  15843  climcndslem1  15862  climcndslem2  15863  cvgrat  15896  clim2prod  15901  prodfn0  15907  prodfrec  15908  ntrivcvgfvn0  15912  fprodabs  15987  fprod2d  15994  binomfallfac  16054  bpolycl  16065  fprodefsum  16108  demoivreALT  16216  ruclem8  16252  ruclem9  16253  dvdsfac  16343  bitsinv1  16459  sadcadd  16475  sadadd2  16477  saddisjlem  16481  smuval2  16499  smupvallem  16500  smu01lem  16502  smupval  16505  smueqlem  16507  smumullem  16509  rplpwr  16575  nn0seqcvgd  16587  seq1st  16588  alginv  16592  algcvga  16596  algfx  16597  prmdvdsexp  16733  prmfac1  16738  eulerthlem2  16800  pcmpt  16911  pcfac  16918  prmpwdvds  16923  prmreclem4  16938  vdwlem10  17009  ramcl  17048  mreexexd  17663  frmdgsum  18879  mulgnnass  19134  mhmmulg  19140  gsumwrev  19389  gsmsymgrfix  19451  gsmsymgreq  19455  efginvrel2  19750  efgsrel  19757  gsum2dlem2  19994  ablfac1eulem  20097  pgpfac  20109  gsumle  20168  srgmulgass  20246  srgpcomp  20247  srgbinom  20260  lmodvsmmulgdi  20944  cnfldexp  21437  ofldchr  21608  assamulgscm  21933  mplcoe1  22070  mplcoe3  22071  mplcoe5  22073  mptcoe1fsupp  22257  coe1fzgsumdlem  22346  coe1fzgsumd  22347  gsummoncoe1  22351  evl1gsumdlem  22399  evl1gsumd  22400  mdetunilem9  22660  mptcoe1matfsupp  22842  mp2pm2mplem4  22849  chpdmat  22881  tgcl  23009  fiuncmp  23444  2ndcsep  23499  1stcelcls  23501  ptcmpfi  23853  tmdgsum  24135  fsumcn  24912  caubl  25350  caublcls  25351  ovolunlem1a  25538  ovolfiniun  25543  volfiniun  25589  voliunlem1  25592  volsuplem  25597  volsup  25598  dyadmax  25640  itgfsum  25869  dvnadd  25971  cpnord  25977  dvnfre  25994  dvmptfsum  26017  ply1divex  26177  fta1g  26210  plyco  26281  dgrcolem1  26313  dgrco  26315  dvnply2  26328  plydivex  26338  aaliou3lem2  26384  dvntaylp  26411  taylthlem1  26413  cxpmul2  26731  jensen  27030  ftalem2  27115  bcmono  27318  bposlem5  27329  lgsquad2lem2  27426  dchrisumlem1  27530  dchrisum0flb  27551  pntpbnd1  27627  pntlemf  27646  qabvle  27666  qabvexp  27667  ostthlem2  27669  ostth2lem2  27675  nosupbnd1lem5  27753  noinfbnd1lem5  27768  precsexlem8  28284  precsexlem9  28285  om2noseqrdg  28374  n0addscl  28414  n0mulscl  28415  eucliddivs  28446  peano5uzs  28474  expscllem  28500  expadds  28505  expsne0  28506  expsgt0  28507  pw2cut  28530  pw2cut2  28532  rusgrnumwwlk  30124  eupth2lems  30386  eupth2  30387  ipasslem1  30980  mdslmd1lem1  32474  mdslmd1lem2  32475  iuninc  32709  ssrelf  32767  nn0min  32973  nexple  32996  gsumwun  33217  gsumvsca1  33367  gsumvsca2  33368  domnprodn0  33420  unitprodclb  33536  1arithufdlem3  33703  cmppcmp  34116  esumfzf  34327  sseqp1  34653  rrvsum  34712  signstfvc  34832  bnj1174  35262  lfuhgr2  35433  subfacp1lem6  35499  mrsubvrs  35836  bccolsum  36053  iprodefisumlem  36054  faclimlem1  36057  onsuct0  36765  findfvcl  36776  poimirlem28  38111  sdclem2  38205  seqpo  38210  incsequz  38211  mettrifi  38220  heiborlem4  38277  bfplem1  38285  pclfinclN  40538  uzindd  42559  indstrd  42774  sn-sup2  43077  incssnn0  43256  mzpexpmpt  43290  pell14qrexpclnn0  43407  monotuz  43482  rmxypos  43488  jm2.17a  43501  jm2.17b  43502  rmygeid  43505  jm2.18  43529  jm2.19lem3  43532  jm2.15nn0  43544  jm2.16nn0  43545  dfac11  43603  pwslnm  43635  hbtlem5  43669  cnsrexpcl  43706  cantnfresb  43865  onmcl  43872  naddonnn  43936  relexpxpnnidm  44243  relexpiidm  44244  relexpss1d  44245  iunrelexpmin1  44248  relexpmulnn  44249  iunrelexpmin2  44252  relexp0a  44256  trclimalb2  44266  dvgrat  44852  relpfrlem  45493  trfr  45502  lmodvsmdi  48965  tfis2d  50265