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  4314  ssrel  5780  ssrelOLD  5781  ssrel2  5783  ssrelrel  5794  funfvima2  7229  isofrlem  7333  dfwe2  7757  tfindsg  7846  tfinds2  7849  tfinds3  7850  trom  7860  findsg  7886  finds2  7887  xpord3inddlem  8136  fpr3g  8266  wfr3g  8303  tfrlem1  8372  tfr3  8395  tz7.48lem  8437  oaordi  8542  oeordi  8583  nnaordi  8614  nnawordi  8617  naddssim  8680  nneneq  9205  nneneqOLD  9217  ac6sfi  9283  domunfican  9316  fodomfi  9321  finsschain  9355  marypha1lem  9424  inf3lem2  9620  inf3lem5  9623  cantnfval2  9660  cantnflt  9663  cantnfp1lem3  9671  cnfcom  9691  ttrclss  9711  ttrclselem2  9717  frr3g  9747  dfac12lem3  10136  ackbij1lem16  10226  sornom  10268  infpssrlem4  10297  fin23lem34  10337  fin23lem36  10339  isf32lem1  10344  isf32lem2  10345  zorn2lem4  10490  zorn2lem5  10491  zorn2lem6  10492  zorn2lem7  10493  ttukeylem5  10504  pwfseqlem3  10651  wunfi  10712  grudomon  10808  prlem934  11024  sup2  12166  nnindd  12228  nnaddcl  12231  nnmulcl  12232  nnne0  12242  peano5uzi  12647  uzind2  12651  nn0indd  12655  fzind  12656  zindd  12659  fzindd  12660  uzaddcl  12884  uzwo  12891  om2uzlti  13911  seqcaopr3  13999  seqf1olem2a  14002  seqf1o  14005  ser1const  14020  expcllem  14034  expeq0  14054  mulexp  14063  expadd  14066  expmul  14069  expmordi  14128  leexp2r  14135  leexp1a  14136  bernneq  14188  modexp  14197  facdiv  14243  facwordi  14245  faclbnd  14246  faclbnd4lem4  14252  hashgadd  14333  hashmap  14391  hashf1lem2  14413  hashf1  14414  seqcoll  14421  cshweqrep  14767  relexpsucnnl  14973  relexpcnv  14978  relexpnndm  14984  relexpaddnn  14994  rlimsqzlem  15591  lo1le  15594  iseraltlem2  15625  fsum2d  15713  modfsummod  15736  fsumabs  15743  fsumrlim  15753  fsumo1  15754  fsumiun  15763  binom  15772  climcndslem1  15791  climcndslem2  15792  cvgrat  15825  clim2prod  15830  prodfn0  15836  prodfrec  15837  ntrivcvgfvn0  15841  fprodabs  15914  fprod2d  15921  binomfallfac  15981  bpolycl  15992  fprodefsum  16034  demoivreALT  16140  ruclem8  16176  ruclem9  16177  dvdsfac  16265  bitsinv1  16379  sadcadd  16395  sadadd2  16397  saddisjlem  16401  smuval2  16419  smupvallem  16420  smu01lem  16422  smupval  16425  smueqlem  16427  smumullem  16429  rplpwr  16495  nn0seqcvgd  16503  seq1st  16504  alginv  16508  algcvga  16512  algfx  16513  prmdvdsexp  16648  prmfac1  16654  eulerthlem2  16711  pcmpt  16821  pcfac  16828  prmpwdvds  16833  prmreclem4  16848  vdwlem10  16919  ramcl  16958  mreexexd  17588  frmdgsum  18739  mulgnnass  18983  mhmmulg  18989  gsumwrev  19227  gsmsymgrfix  19290  gsmsymgreq  19294  efginvrel2  19589  efgsrel  19596  gsum2dlem2  19833  ablfac1eulem  19936  pgpfac  19948  srgmulgass  20033  srgpcomp  20034  srgbinom  20047  lmodvsmmulgdi  20499  cnfldexp  20970  assamulgscm  21446  mplcoe1  21583  mplcoe3  21584  mplcoe5  21586  mptcoe1fsupp  21730  coe1fzgsumdlem  21816  coe1fzgsumd  21817  gsummoncoe1  21819  evl1gsumdlem  21866  evl1gsumd  21867  mdetunilem9  22113  mptcoe1matfsupp  22295  mp2pm2mplem4  22302  chpdmat  22334  tgcl  22463  fiuncmp  22899  2ndcsep  22954  1stcelcls  22956  ptcmpfi  23308  tmdgsum  23590  fsumcn  24377  caubl  24816  caublcls  24817  ovolunlem1a  25004  ovolfiniun  25009  volfiniun  25055  voliunlem1  25058  volsuplem  25063  volsup  25064  dyadmax  25106  itgfsum  25335  dvnadd  25437  cpnord  25443  dvnfre  25460  dvmptfsum  25483  ply1divex  25645  fta1g  25676  plyco  25746  dgrcolem1  25778  dgrco  25780  dvnply2  25791  plydivex  25801  aaliou3lem2  25847  dvntaylp  25874  taylthlem1  25876  cxpmul2  26188  jensen  26482  ftalem2  26567  bcmono  26769  bposlem5  26780  lgsquad2lem2  26877  dchrisumlem1  26981  dchrisum0flb  27002  pntpbnd1  27078  pntlemf  27097  qabvle  27117  qabvexp  27118  ostthlem2  27120  ostth2lem2  27126  nosupbnd1lem5  27204  noinfbnd1lem5  27219  precsexlem8  27649  precsexlem9  27650  rusgrnumwwlk  29218  eupth2lems  29480  eupth2  29481  ipasslem1  30071  mdslmd1lem1  31565  mdslmd1lem2  31566  iuninc  31779  ssrelf  31831  nn0min  32013  gsumle  32229  gsumvsca1  32358  gsumvsca2  32359  ofldchr  32420  cmppcmp  32826  nexple  32995  esumfzf  33055  sseqp1  33382  rrvsum  33441  signstfvc  33573  bnj1174  34002  lfuhgr2  34097  subfacp1lem6  34164  mrsubvrs  34501  bccolsum  34697  iprodefisumlem  34698  faclimlem1  34701  onsuct0  35314  findfvcl  35325  poimirlem28  36504  sdclem2  36598  seqpo  36603  incsequz  36604  mettrifi  36613  heiborlem4  36670  bfplem1  36678  pclfinclN  38809  uzindd  40830  nnaddcom  41179  nnadddir  41181  nnmulcom  41183  sn-sup2  41338  incssnn0  41434  mzpexpmpt  41468  pell14qrexpclnn0  41589  monotuz  41665  rmxypos  41671  jm2.17a  41684  jm2.17b  41685  rmygeid  41688  jm2.18  41712  jm2.19lem3  41715  jm2.15nn0  41727  jm2.16nn0  41728  dfac11  41789  pwslnm  41821  hbtlem5  41855  cnsrexpcl  41892  cantnfresb  42059  onmcl  42066  naddonnn  42131  relexpxpnnidm  42439  relexpiidm  42440  relexpss1d  42441  iunrelexpmin1  42444  relexpmulnn  42445  iunrelexpmin2  42448  relexp0a  42452  trclimalb2  42462  dvgrat  43056  lmodvsmdi  47011  tfis2d  47678