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  847  minimp  1623  cbv1v  2341  cbv1  2407  ralimdva  3150  reuss2  4267  ssrel  5732  ssrel2  5734  ssrelrel  5745  funfvima2  7179  isofrlem  7288  dfwe2  7721  tfindsg  7805  tfinds2  7808  tfinds3  7809  trom  7819  findsg  7841  finds2  7842  xpord3inddlem  8097  fpr3g  8228  wfr3g  8262  tfrlem1  8308  tfr3  8331  tz7.48lem  8373  oaordi  8474  oeordi  8516  nnaordi  8547  nnawordi  8550  naddssim  8614  naddoa  8631  nneneq  9133  ac6sfi  9187  fodomfi  9215  domunfican  9225  fodomfiOLD  9233  finsschain  9262  marypha1lem  9339  inf3lem2  9541  inf3lem5  9544  cantnfval2  9581  cantnflt  9584  cantnfp1lem3  9592  cnfcom  9612  ttrclss  9632  ttrclselem2  9638  frr3g  9671  dfac12lem3  10059  ackbij1lem16  10147  sornom  10190  infpssrlem4  10219  fin23lem34  10259  fin23lem36  10261  isf32lem1  10266  isf32lem2  10267  zorn2lem4  10412  zorn2lem5  10413  zorn2lem6  10414  zorn2lem7  10415  ttukeylem5  10426  pwfseqlem3  10574  wunfi  10635  grudomon  10731  prlem934  10947  sup2  12103  nnindd  12185  nnaddcl  12188  nnmulcl  12189  nnaddcom  12192  nnne0  12202  nnadddir  12224  nnmulcom  12226  peano5uzi  12609  uzind2  12613  nn0indd  12617  fzind  12618  zindd  12621  fzindd  12622  uzaddcl  12845  uzwo  12852  om2uzlti  13903  seqcaopr3  13990  seqf1olem2a  13993  seqf1o  13996  ser1const  14011  expcllem  14025  expeq0  14045  mulexp  14054  expadd  14057  expmul  14060  expmordi  14120  leexp2r  14127  leexp1a  14128  bernneq  14182  modexp  14191  facdiv  14240  facwordi  14242  faclbnd  14243  faclbnd4lem4  14249  hashgadd  14330  hashmap  14388  hashf1lem2  14409  hashf1  14410  seqcoll  14417  cshweqrep  14774  relexpsucnnl  14983  relexpcnv  14988  relexpnndm  14994  relexpaddnn  15004  rlimsqzlem  15602  lo1le  15605  iseraltlem2  15636  fsum2d  15724  modfsummod  15748  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  binom  15786  climcndslem1  15805  climcndslem2  15806  cvgrat  15839  clim2prod  15844  prodfn0  15850  prodfrec  15851  ntrivcvgfvn0  15855  fprodabs  15930  fprod2d  15937  binomfallfac  15997  bpolycl  16008  fprodefsum  16051  demoivreALT  16159  ruclem8  16195  ruclem9  16196  dvdsfac  16286  bitsinv1  16402  sadcadd  16418  sadadd2  16420  saddisjlem  16424  smuval2  16442  smupvallem  16443  smu01lem  16445  smupval  16448  smueqlem  16450  smumullem  16452  rplpwr  16518  nn0seqcvgd  16530  seq1st  16531  alginv  16535  algcvga  16539  algfx  16540  prmdvdsexp  16676  prmfac1  16681  eulerthlem2  16743  pcmpt  16854  pcfac  16861  prmpwdvds  16866  prmreclem4  16881  vdwlem10  16952  ramcl  16991  mreexexd  17605  frmdgsum  18821  mulgnnass  19076  mhmmulg  19082  gsumwrev  19332  gsmsymgrfix  19394  gsmsymgreq  19398  efginvrel2  19693  efgsrel  19700  gsum2dlem2  19937  ablfac1eulem  20040  pgpfac  20052  gsumle  20111  srgmulgass  20189  srgpcomp  20190  srgbinom  20203  lmodvsmmulgdi  20883  cnfldexp  21394  ofldchr  21566  assamulgscm  21891  mplcoe1  22025  mplcoe3  22026  mplcoe5  22028  mptcoe1fsupp  22189  coe1fzgsumdlem  22278  coe1fzgsumd  22279  gsummoncoe1  22283  evl1gsumdlem  22331  evl1gsumd  22332  mdetunilem9  22595  mptcoe1matfsupp  22777  mp2pm2mplem4  22784  chpdmat  22816  tgcl  22944  fiuncmp  23379  2ndcsep  23434  1stcelcls  23436  ptcmpfi  23788  tmdgsum  24070  fsumcn  24847  caubl  25285  caublcls  25286  ovolunlem1a  25473  ovolfiniun  25478  volfiniun  25524  voliunlem1  25527  volsuplem  25532  volsup  25533  dyadmax  25575  itgfsum  25804  dvnadd  25906  cpnord  25912  dvnfre  25929  dvmptfsum  25952  ply1divex  26112  fta1g  26145  plyco  26216  dgrcolem1  26248  dgrco  26250  dvnply2  26264  plydivex  26274  aaliou3lem2  26320  dvntaylp  26348  taylthlem1  26350  cxpmul2  26666  jensen  26966  ftalem2  27051  bcmono  27254  bposlem5  27265  lgsquad2lem2  27362  dchrisumlem1  27466  dchrisum0flb  27487  pntpbnd1  27563  pntlemf  27582  qabvle  27602  qabvexp  27603  ostthlem2  27605  ostth2lem2  27611  nosupbnd1lem5  27690  noinfbnd1lem5  27705  precsexlem8  28220  precsexlem9  28221  om2noseqrdg  28310  n0addscl  28350  n0mulscl  28351  eucliddivs  28382  peano5uzs  28410  expscllem  28436  expadds  28441  expsne0  28442  expsgt0  28443  pw2cut  28466  pw2cut2  28468  rusgrnumwwlk  30061  eupth2lems  30323  eupth2  30324  ipasslem1  30917  mdslmd1lem1  32411  mdslmd1lem2  32412  iuninc  32645  ssrelf  32703  nn0min  32909  nexple  32932  gsumwun  33152  gsumvsca1  33302  gsumvsca2  33303  domnprodn0  33351  unitprodclb  33464  1arithufdlem3  33621  cmppcmp  34018  esumfzf  34229  sseqp1  34555  rrvsum  34614  signstfvc  34734  bnj1174  35161  lfuhgr2  35317  subfacp1lem6  35383  mrsubvrs  35720  bccolsum  35937  iprodefisumlem  35938  faclimlem1  35941  onsuct0  36639  findfvcl  36650  poimirlem28  37983  sdclem2  38077  seqpo  38082  incsequz  38083  mettrifi  38092  heiborlem4  38149  bfplem1  38157  pclfinclN  40410  uzindd  42431  indstrd  42646  sn-sup2  42950  incssnn0  43157  mzpexpmpt  43191  pell14qrexpclnn0  43312  monotuz  43387  rmxypos  43393  jm2.17a  43406  jm2.17b  43407  rmygeid  43410  jm2.18  43434  jm2.19lem3  43437  jm2.15nn0  43449  jm2.16nn0  43450  dfac11  43508  pwslnm  43540  hbtlem5  43574  cnsrexpcl  43611  cantnfresb  43770  onmcl  43777  naddonnn  43841  relexpxpnnidm  44148  relexpiidm  44149  relexpss1d  44150  iunrelexpmin1  44153  relexpmulnn  44154  iunrelexpmin2  44157  relexp0a  44161  trclimalb2  44171  dvgrat  44757  relpfrlem  45398  trfr  45407  lmodvsmdi  48867  tfis2d  50167