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  2340  cbv1  2406  ralimdva  3149  reuss2  4266  ssrel  5739  ssrel2  5741  ssrelrel  5752  funfvima2  7186  isofrlem  7295  dfwe2  7728  tfindsg  7812  tfinds2  7815  tfinds3  7816  trom  7826  findsg  7848  finds2  7849  xpord3inddlem  8104  fpr3g  8235  wfr3g  8269  tfrlem1  8315  tfr3  8338  tz7.48lem  8380  oaordi  8481  oeordi  8523  nnaordi  8554  nnawordi  8557  naddssim  8621  naddoa  8638  nneneq  9140  ac6sfi  9194  fodomfi  9222  domunfican  9232  fodomfiOLD  9240  finsschain  9269  marypha1lem  9346  inf3lem2  9550  inf3lem5  9553  cantnfval2  9590  cantnflt  9593  cantnfp1lem3  9601  cnfcom  9621  ttrclss  9641  ttrclselem2  9647  frr3g  9680  dfac12lem3  10068  ackbij1lem16  10156  sornom  10199  infpssrlem4  10228  fin23lem34  10268  fin23lem36  10270  isf32lem1  10275  isf32lem2  10276  zorn2lem4  10421  zorn2lem5  10422  zorn2lem6  10423  zorn2lem7  10424  ttukeylem5  10435  pwfseqlem3  10583  wunfi  10644  grudomon  10740  prlem934  10956  sup2  12112  nnindd  12194  nnaddcl  12197  nnmulcl  12198  nnaddcom  12201  nnne0  12211  nnadddir  12233  nnmulcom  12235  peano5uzi  12618  uzind2  12622  nn0indd  12626  fzind  12627  zindd  12630  fzindd  12631  uzaddcl  12854  uzwo  12861  om2uzlti  13912  seqcaopr3  13999  seqf1olem2a  14002  seqf1o  14005  ser1const  14020  expcllem  14034  expeq0  14054  mulexp  14063  expadd  14066  expmul  14069  expmordi  14129  leexp2r  14136  leexp1a  14137  bernneq  14191  modexp  14200  facdiv  14249  facwordi  14251  faclbnd  14252  faclbnd4lem4  14258  hashgadd  14339  hashmap  14397  hashf1lem2  14418  hashf1  14419  seqcoll  14426  cshweqrep  14783  relexpsucnnl  14992  relexpcnv  14997  relexpnndm  15003  relexpaddnn  15013  rlimsqzlem  15611  lo1le  15614  iseraltlem2  15645  fsum2d  15733  modfsummod  15757  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  binom  15795  climcndslem1  15814  climcndslem2  15815  cvgrat  15848  clim2prod  15853  prodfn0  15859  prodfrec  15860  ntrivcvgfvn0  15864  fprodabs  15939  fprod2d  15946  binomfallfac  16006  bpolycl  16017  fprodefsum  16060  demoivreALT  16168  ruclem8  16204  ruclem9  16205  dvdsfac  16295  bitsinv1  16411  sadcadd  16427  sadadd2  16429  saddisjlem  16433  smuval2  16451  smupvallem  16452  smu01lem  16454  smupval  16457  smueqlem  16459  smumullem  16461  rplpwr  16527  nn0seqcvgd  16539  seq1st  16540  alginv  16544  algcvga  16548  algfx  16549  prmdvdsexp  16685  prmfac1  16690  eulerthlem2  16752  pcmpt  16863  pcfac  16870  prmpwdvds  16875  prmreclem4  16890  vdwlem10  16961  ramcl  17000  mreexexd  17614  frmdgsum  18830  mulgnnass  19085  mhmmulg  19091  gsumwrev  19341  gsmsymgrfix  19403  gsmsymgreq  19407  efginvrel2  19702  efgsrel  19709  gsum2dlem2  19946  ablfac1eulem  20049  pgpfac  20061  gsumle  20120  srgmulgass  20198  srgpcomp  20199  srgbinom  20212  lmodvsmmulgdi  20892  cnfldexp  21385  ofldchr  21556  assamulgscm  21881  mplcoe1  22015  mplcoe3  22016  mplcoe5  22018  mptcoe1fsupp  22179  coe1fzgsumdlem  22268  coe1fzgsumd  22269  gsummoncoe1  22273  evl1gsumdlem  22321  evl1gsumd  22322  mdetunilem9  22585  mptcoe1matfsupp  22767  mp2pm2mplem4  22774  chpdmat  22806  tgcl  22934  fiuncmp  23369  2ndcsep  23424  1stcelcls  23426  ptcmpfi  23778  tmdgsum  24060  fsumcn  24837  caubl  25275  caublcls  25276  ovolunlem1a  25463  ovolfiniun  25468  volfiniun  25514  voliunlem1  25517  volsuplem  25522  volsup  25523  dyadmax  25565  itgfsum  25794  dvnadd  25896  cpnord  25902  dvnfre  25919  dvmptfsum  25942  ply1divex  26102  fta1g  26135  plyco  26206  dgrcolem1  26238  dgrco  26240  dvnply2  26253  plydivex  26263  aaliou3lem2  26309  dvntaylp  26336  taylthlem1  26338  cxpmul2  26653  jensen  26952  ftalem2  27037  bcmono  27240  bposlem5  27251  lgsquad2lem2  27348  dchrisumlem1  27452  dchrisum0flb  27473  pntpbnd1  27549  pntlemf  27568  qabvle  27588  qabvexp  27589  ostthlem2  27591  ostth2lem2  27597  nosupbnd1lem5  27676  noinfbnd1lem5  27691  precsexlem8  28206  precsexlem9  28207  om2noseqrdg  28296  n0addscl  28336  n0mulscl  28337  eucliddivs  28368  peano5uzs  28396  expscllem  28422  expadds  28427  expsne0  28428  expsgt0  28429  pw2cut  28452  pw2cut2  28454  rusgrnumwwlk  30046  eupth2lems  30308  eupth2  30309  ipasslem1  30902  mdslmd1lem1  32396  mdslmd1lem2  32397  iuninc  32630  ssrelf  32688  nn0min  32894  nexple  32917  gsumwun  33137  gsumvsca1  33287  gsumvsca2  33288  domnprodn0  33336  unitprodclb  33449  1arithufdlem3  33606  cmppcmp  34002  esumfzf  34213  sseqp1  34539  rrvsum  34598  signstfvc  34718  bnj1174  35145  lfuhgr2  35301  subfacp1lem6  35367  mrsubvrs  35704  bccolsum  35921  iprodefisumlem  35922  faclimlem1  35925  onsuct0  36623  findfvcl  36634  poimirlem28  37969  sdclem2  38063  seqpo  38068  incsequz  38069  mettrifi  38078  heiborlem4  38135  bfplem1  38143  pclfinclN  40396  uzindd  42417  indstrd  42632  sn-sup2  42936  incssnn0  43143  mzpexpmpt  43177  pell14qrexpclnn0  43294  monotuz  43369  rmxypos  43375  jm2.17a  43388  jm2.17b  43389  rmygeid  43392  jm2.18  43416  jm2.19lem3  43419  jm2.15nn0  43431  jm2.16nn0  43432  dfac11  43490  pwslnm  43522  hbtlem5  43556  cnsrexpcl  43593  cantnfresb  43752  onmcl  43759  naddonnn  43823  relexpxpnnidm  44130  relexpiidm  44131  relexpss1d  44132  iunrelexpmin1  44135  relexpmulnn  44136  iunrelexpmin2  44139  relexp0a  44143  trclimalb2  44153  dvgrat  44739  relpfrlem  45380  trfr  45389  lmodvsmdi  48855  tfis2d  50155