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  1616  cbv1v  2327  cbv1  2396  ralimdva  3157  reuss2  4318  ssrel  5788  ssrelOLD  5789  ssrel2  5791  ssrelrel  5802  funfvima2  7248  isofrlem  7352  dfwe2  7782  tfindsg  7871  tfinds2  7874  tfinds3  7875  trom  7885  findsg  7910  finds2  7911  xpord3inddlem  8168  fpr3g  8300  wfr3g  8337  tfrlem1  8406  tfr3  8429  tz7.48lem  8471  oaordi  8576  oeordi  8617  nnaordi  8648  nnawordi  8651  naddssim  8715  nneneq  9243  nneneqOLD  9255  ac6sfi  9321  fodomfi  9352  domunfican  9363  fodomfiOLD  9372  finsschain  9403  marypha1lem  9476  inf3lem2  9672  inf3lem5  9675  cantnfval2  9712  cantnflt  9715  cantnfp1lem3  9723  cnfcom  9743  ttrclss  9763  ttrclselem2  9769  frr3g  9799  dfac12lem3  10188  ackbij1lem16  10278  sornom  10320  infpssrlem4  10349  fin23lem34  10389  fin23lem36  10391  isf32lem1  10396  isf32lem2  10397  zorn2lem4  10542  zorn2lem5  10543  zorn2lem6  10544  zorn2lem7  10545  ttukeylem5  10556  pwfseqlem3  10703  wunfi  10764  grudomon  10860  prlem934  11076  sup2  12222  nnindd  12284  nnaddcl  12287  nnmulcl  12288  nnne0  12298  peano5uzi  12703  uzind2  12707  nn0indd  12711  fzind  12712  zindd  12715  fzindd  12716  uzaddcl  12940  uzwo  12947  om2uzlti  13970  seqcaopr3  14057  seqf1olem2a  14060  seqf1o  14063  ser1const  14078  expcllem  14092  expeq0  14112  mulexp  14121  expadd  14124  expmul  14127  expmordi  14186  leexp2r  14193  leexp1a  14194  bernneq  14246  modexp  14255  facdiv  14304  facwordi  14306  faclbnd  14307  faclbnd4lem4  14313  hashgadd  14394  hashmap  14452  hashf1lem2  14475  hashf1  14476  seqcoll  14483  cshweqrep  14829  relexpsucnnl  15035  relexpcnv  15040  relexpnndm  15046  relexpaddnn  15056  rlimsqzlem  15653  lo1le  15656  iseraltlem2  15687  fsum2d  15775  modfsummod  15798  fsumabs  15805  fsumrlim  15815  fsumo1  15816  fsumiun  15825  binom  15834  climcndslem1  15853  climcndslem2  15854  cvgrat  15887  clim2prod  15892  prodfn0  15898  prodfrec  15899  ntrivcvgfvn0  15903  fprodabs  15976  fprod2d  15983  binomfallfac  16043  bpolycl  16054  fprodefsum  16097  demoivreALT  16203  ruclem8  16239  ruclem9  16240  dvdsfac  16328  bitsinv1  16442  sadcadd  16458  sadadd2  16460  saddisjlem  16464  smuval2  16482  smupvallem  16483  smu01lem  16485  smupval  16488  smueqlem  16490  smumullem  16492  rplpwr  16559  nn0seqcvgd  16571  seq1st  16572  alginv  16576  algcvga  16580  algfx  16581  prmdvdsexp  16716  prmfac1  16722  eulerthlem2  16784  pcmpt  16894  pcfac  16901  prmpwdvds  16906  prmreclem4  16921  vdwlem10  16992  ramcl  17031  mreexexd  17661  frmdgsum  18852  mulgnnass  19103  mhmmulg  19109  gsumwrev  19363  gsmsymgrfix  19426  gsmsymgreq  19430  efginvrel2  19725  efgsrel  19732  gsum2dlem2  19969  ablfac1eulem  20072  pgpfac  20084  srgmulgass  20200  srgpcomp  20201  srgbinom  20214  lmodvsmmulgdi  20873  cnfldexp  21396  assamulgscm  21898  mplcoe1  22044  mplcoe3  22045  mplcoe5  22047  mptcoe1fsupp  22205  coe1fzgsumdlem  22294  coe1fzgsumd  22295  gsummoncoe1  22299  evl1gsumdlem  22347  evl1gsumd  22348  mdetunilem9  22613  mptcoe1matfsupp  22795  mp2pm2mplem4  22802  chpdmat  22834  tgcl  22963  fiuncmp  23399  2ndcsep  23454  1stcelcls  23456  ptcmpfi  23808  tmdgsum  24090  fsumcn  24879  caubl  25327  caublcls  25328  ovolunlem1a  25516  ovolfiniun  25521  volfiniun  25567  voliunlem1  25570  volsuplem  25575  volsup  25576  dyadmax  25618  itgfsum  25847  dvnadd  25950  cpnord  25956  dvnfre  25975  dvmptfsum  25998  ply1divex  26164  fta1g  26197  plyco  26268  dgrcolem1  26301  dgrco  26303  dvnply2  26315  plydivex  26325  aaliou3lem2  26371  dvntaylp  26399  taylthlem1  26401  cxpmul2  26716  jensen  27017  ftalem2  27102  bcmono  27306  bposlem5  27317  lgsquad2lem2  27414  dchrisumlem1  27518  dchrisum0flb  27539  pntpbnd1  27615  pntlemf  27634  qabvle  27654  qabvexp  27655  ostthlem2  27657  ostth2lem2  27663  nosupbnd1lem5  27742  noinfbnd1lem5  27757  precsexlem8  28213  precsexlem9  28214  om2noseqrdg  28278  n0addscl  28313  n0mulscl  28314  rusgrnumwwlk  29909  eupth2lems  30171  eupth2  30172  ipasslem1  30764  mdslmd1lem1  32258  mdslmd1lem2  32259  iuninc  32481  ssrelf  32535  nn0min  32721  gsumle  32959  gsumvsca1  33090  gsumvsca2  33091  domnprodn0  33130  ofldchr  33192  unitprodclb  33264  1arithufdlem3  33421  cmppcmp  33673  nexple  33842  esumfzf  33902  sseqp1  34229  rrvsum  34288  signstfvc  34420  bnj1174  34848  lfuhgr2  34946  subfacp1lem6  35013  mrsubvrs  35350  bccolsum  35561  iprodefisumlem  35562  faclimlem1  35565  onsuct0  36153  findfvcl  36164  poimirlem28  37349  sdclem2  37443  seqpo  37448  incsequz  37449  mettrifi  37458  heiborlem4  37515  bfplem1  37523  pclfinclN  39649  uzindd  41675  nnaddcom  42082  nnadddir  42084  nnmulcom  42086  sn-sup2  42251  incssnn0  42368  mzpexpmpt  42402  pell14qrexpclnn0  42523  monotuz  42599  rmxypos  42605  jm2.17a  42618  jm2.17b  42619  rmygeid  42622  jm2.18  42646  jm2.19lem3  42649  jm2.15nn0  42661  jm2.16nn0  42662  dfac11  42723  pwslnm  42755  hbtlem5  42789  cnsrexpcl  42826  cantnfresb  42990  onmcl  42997  naddonnn  43062  relexpxpnnidm  43370  relexpiidm  43371  relexpss1d  43372  iunrelexpmin1  43375  relexpmulnn  43376  iunrelexpmin2  43379  relexp0a  43383  trclimalb2  43393  dvgrat  43986  lmodvsmdi  47761  tfis2d  48426