Theorem a2d 30

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 18	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  44  imim2d  58  imim3i  65  loowoz  113  animpimp2impd  859  minimp  1644  cbv1v  2370  cbv1  2436  ralimdva  3177  reuss2  4281  ssrel  5760  ssrel2  5762  ssrelrel  5773  funfvima2  7219  isofrlem  7328  dfwe2  7761  tfindsg  7845  tfinds2  7848  tfinds3  7849  trom  7859  findsg  7882  finds2  7883  xpord3inddlem  8138  fpr3g  8270  wfr3g  8304  tfrlem1  8350  tfr3  8374  tz7.48lem  8416  oaordi  8519  oeordi  8561  nnaordi  8592  nnawordi  8595  naddssim  8660  naddoa  8677  nneneq  9178  ac6sfi  9232  fodomfi  9260  domunfican  9269  finsschain  9304  marypha1lem  9381  inf3lem2  9586  inf3lem5  9589  cantnfval2  9626  cantnflt  9629  cantnfp1lem3  9637  cnfcom  9657  ttrclss  9677  ttrclselem2  9683  frr3g  9716  dfac12lem3  10117  ackbij1lem16  10205  sornom  10249  infpssrlem4  10278  fin23lem34  10318  fin23lem36  10320  isf32lem1  10325  isf32lem2  10326  zorn2lem4  10471  zorn2lem5  10472  zorn2lem6  10473  zorn2lem7  10474  ttukeylem5  10485  pwfseqlem3  10633  wunfi  10694  grudomon  10790  prlem934  11006  sup2  12162  nnindd  12244  nnaddcl  12247  nnmulcl  12248  nnaddcom  12251  nnne0  12261  nnadddir  12283  nnmulcom  12285  peano5uzi  12676  uzind2  12680  nn0indd  12684  fzind  12685  zindd  12688  fzindd  12689  uzaddcl  12919  uzwo  12926  om2uzlti  13977  seqcaopr3  14064  seqf1olem2a  14067  seqf1o  14070  ser1const  14085  expcllem  14099  expeq0  14119  mulexp  14128  expadd  14131  expmul  14134  expmordi  14194  leexp2r  14201  leexp1a  14202  bernneq  14256  modexp  14265  facdiv  14314  facwordi  14316  faclbnd  14317  faclbnd4lem4  14323  hashgadd  14404  hashmap  14462  hashf1lem2  14483  hashf1  14484  seqcoll  14491  cshweqrep  14848  relexpsucnnl  15057  relexpcnv  15062  relexpnndm  15068  relexpaddnn  15078  rlimsqzlem  15690  lo1le  15693  iseraltlem2  15724  fsum2d  15812  modfsummod  15836  fsumabs  15843  fsumrlim  15853  fsumo1  15854  fsumiun  15863  binom  15874  climcndslem1  15893  climcndslem2  15894  cvgrat  15927  clim2prod  15932  prodfn0  15938  prodfrec  15939  ntrivcvgfvn0  15943  fprodabs  16018  fprod2d  16025  binomfallfac  16085  bpolycl  16096  fprodefsum  16139  demoivreALT  16247  ruclem8  16283  ruclem9  16284  dvdsfac  16374  bitsinv1  16490  sadcadd  16506  sadadd2  16508  saddisjlem  16512  smuval2  16530  smupvallem  16531  smu01lem  16533  smupval  16536  smueqlem  16538  smumullem  16540  rplpwr  16606  nn0seqcvgd  16618  seq1st  16619  alginv  16623  algcvga  16627  algfx  16628  prmdvdsexp  16764  prmfac1  16769  eulerthlem2  16831  pcmpt  16942  pcfac  16949  prmpwdvds  16954  prmreclem4  16969  vdwlem10  17040  ramcl  17079  mreexexd  17694  frmdgsum  18911  mulgnnass  19166  mhmmulg  19172  gsumwrev  19427  gsmsymgrfix  19489  gsmsymgreq  19493  efginvrel2  19788  efgsrel  19795  gsum2dlem2  20032  ablfac1eulem  20135  pgpfac  20147  gsumle  20206  srgmulgass  20290  srgpcomp  20291  srgbinom  20304  lmodvsmmulgdi  20987  cnfldexp  21515  ofldchr  21686  assamulgscm  22011  mplcoe1  22148  mplcoe3  22149  mplcoe5  22151  mptcoe1fsupp  22335  coe1fzgsumdlem  22424  coe1fzgsumd  22425  gsummoncoe1  22429  evl1gsumdlem  22477  evl1gsumd  22478  mdetunilem9  22738  mptcoe1matfsupp  22920  mp2pm2mplem4  22927  chpdmat  22959  tgcl  23087  fiuncmp  23522  2ndcsep  23577  1stcelcls  23579  ptcmpfi  23931  tmdgsum  24213  fsumcn  24990  caubl  25428  caublcls  25429  ovolunlem1a  25616  ovolfiniun  25621  volfiniun  25667  voliunlem1  25670  volsuplem  25675  volsup  25676  dyadmax  25718  itgfsum  25947  dvnadd  26049  cpnord  26055  dvnfre  26072  dvmptfsum  26095  ply1divex  26255  fta1g  26288  plyco  26359  dgrcolem1  26391  dgrco  26393  dvnply2  26409  plydivex  26419  aaliou3lem2  26465  dvntaylp  26492  taylthlem1  26494  cxpmul2  26812  jensen  27111  ftalem2  27196  bcmono  27399  bposlem5  27410  lgsquad2lem2  27507  dchrisumlem1  27611  dchrisum0flb  27632  pntpbnd1  27708  pntlemf  27727  qabvle  27747  qabvexp  27748  ostthlem2  27750  ostth2lem2  27756  nosupbnd1lem5  27834  noinfbnd1lem5  27849  precsexlem8  28365  precsexlem9  28366  om2noseqrdg  28455  n0addscl  28495  n0mulscl  28496  eucliddivs  28527  peano5uzs  28555  expscllem  28581  expadds  28586  expsne0  28587  expsgt0  28588  pw2cut  28611  pw2cut2  28613  plngrotlem2  29018  rusgrnumwwlk  30236  eupth2lems  30498  eupth2  30499  ipasslem1  31092  mdslmd1lem1  32586  mdslmd1lem2  32587  iuninc  32815  ssrelf  32872  nn0min  33078  nexple  33090  gsumwun  33309  gsumvsca1  33459  gsumvsca2  33460  domnprodn0  33511  unitprodclb  33618  1arithufdlem3  33753  cmppcmp  34165  esumfzf  34376  sseqp1  34702  rrvsum  34761  signstfvc  34878  bnj1174  35308  lfuhgr2  35482  subfacp1lem6  35548  mrsubvrs  35885  bccolsum  36102  iprodefisumlem  36103  faclimlem1  36106  onsuct0  36814  findfvcl  36825  poimirlem28  38159  sdclem2  38253  seqpo  38258  incsequz  38259  mettrifi  38268  heiborlem4  38325  bfplem1  38333  pclfinclN  40586  uzindd  42607  indstrd  42822  sn-sup2  43125  incssnn0  43304  mzpexpmpt  43338  pell14qrexpclnn0  43455  monotuz  43530  rmxypos  43536  jm2.17a  43549  jm2.17b  43550  rmygeid  43553  jm2.18  43577  jm2.19lem3  43580  jm2.15nn0  43592  jm2.16nn0  43593  dfac11  43651  pwslnm  43683  hbtlem5  43717  cnsrexpcl  43754  cantnfresb  43913  onmcl  43920  naddonnn  43984  relexpxpnnidm  44291  relexpiidm  44292  relexpss1d  44293  iunrelexpmin1  44296  relexpmulnn  44297  iunrelexpmin2  44300  relexp0a  44304  trclimalb2  44314  dvgrat  44886  relpfrlem  45527  trfr  45536  lmodvsmdi  49010  tfis2d  50309