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  857  minimp  1640  cbv1v  2366  cbv1  2432  ralimdva  3173  reuss2  4278  ssrel  5753  ssrel2  5755  ssrelrel  5766  funfvima2  7209  isofrlem  7318  dfwe2  7751  tfindsg  7835  tfinds2  7838  tfinds3  7839  trom  7849  findsg  7872  finds2  7873  xpord3inddlem  8127  fpr3g  8259  wfr3g  8293  tfrlem1  8339  tfr3  8363  tz7.48lem  8405  oaordi  8508  oeordi  8550  nnaordi  8581  nnawordi  8584  naddssim  8649  naddoa  8666  nneneq  9168  ac6sfi  9222  fodomfi  9250  domunfican  9260  fodomfiOLD  9268  finsschain  9297  marypha1lem  9374  inf3lem2  9579  inf3lem5  9582  cantnfval2  9619  cantnflt  9622  cantnfp1lem3  9630  cnfcom  9650  ttrclss  9670  ttrclselem2  9676  frr3g  9709  dfac12lem3  10097  ackbij1lem16  10185  sornom  10229  infpssrlem4  10258  fin23lem34  10298  fin23lem36  10300  isf32lem1  10305  isf32lem2  10306  zorn2lem4  10451  zorn2lem5  10452  zorn2lem6  10453  zorn2lem7  10454  ttukeylem5  10465  pwfseqlem3  10613  wunfi  10674  grudomon  10770  prlem934  10986  sup2  12143  nnindd  12225  nnaddcl  12228  nnmulcl  12229  nnaddcom  12232  nnne0  12242  nnadddir  12264  nnmulcom  12266  peano5uzi  12657  uzind2  12661  nn0indd  12665  fzind  12666  zindd  12669  fzindd  12670  uzaddcl  12900  uzwo  12907  om2uzlti  13958  seqcaopr3  14045  seqf1olem2a  14048  seqf1o  14051  ser1const  14066  expcllem  14080  expeq0  14100  mulexp  14109  expadd  14112  expmul  14115  expmordi  14175  leexp2r  14182  leexp1a  14183  bernneq  14237  modexp  14246  facdiv  14295  facwordi  14297  faclbnd  14298  faclbnd4lem4  14304  hashgadd  14385  hashmap  14443  hashf1lem2  14464  hashf1  14465  seqcoll  14472  cshweqrep  14829  relexpsucnnl  15038  relexpcnv  15043  relexpnndm  15049  relexpaddnn  15059  rlimsqzlem  15657  lo1le  15660  iseraltlem2  15691  fsum2d  15779  modfsummod  15803  fsumabs  15810  fsumrlim  15820  fsumo1  15821  fsumiun  15830  binom  15841  climcndslem1  15860  climcndslem2  15861  cvgrat  15894  clim2prod  15899  prodfn0  15905  prodfrec  15906  ntrivcvgfvn0  15910  fprodabs  15985  fprod2d  15992  binomfallfac  16052  bpolycl  16063  fprodefsum  16106  demoivreALT  16214  ruclem8  16250  ruclem9  16251  dvdsfac  16341  bitsinv1  16457  sadcadd  16473  sadadd2  16475  saddisjlem  16479  smuval2  16497  smupvallem  16498  smu01lem  16500  smupval  16503  smueqlem  16505  smumullem  16507  rplpwr  16573  nn0seqcvgd  16585  seq1st  16586  alginv  16590  algcvga  16594  algfx  16595  prmdvdsexp  16731  prmfac1  16736  eulerthlem2  16798  pcmpt  16909  pcfac  16916  prmpwdvds  16921  prmreclem4  16936  vdwlem10  17007  ramcl  17046  mreexexd  17661  frmdgsum  18877  mulgnnass  19132  mhmmulg  19138  gsumwrev  19387  gsmsymgrfix  19449  gsmsymgreq  19453  efginvrel2  19748  efgsrel  19755  gsum2dlem2  19992  ablfac1eulem  20095  pgpfac  20107  gsumle  20166  srgmulgass  20244  srgpcomp  20245  srgbinom  20258  lmodvsmmulgdi  20942  cnfldexp  21435  ofldchr  21606  assamulgscm  21931  mplcoe1  22068  mplcoe3  22069  mplcoe5  22071  mptcoe1fsupp  22255  coe1fzgsumdlem  22344  coe1fzgsumd  22345  gsummoncoe1  22349  evl1gsumdlem  22397  evl1gsumd  22398  mdetunilem9  22658  mptcoe1matfsupp  22840  mp2pm2mplem4  22847  chpdmat  22879  tgcl  23007  fiuncmp  23442  2ndcsep  23497  1stcelcls  23499  ptcmpfi  23851  tmdgsum  24133  fsumcn  24910  caubl  25348  caublcls  25349  ovolunlem1a  25536  ovolfiniun  25541  volfiniun  25587  voliunlem1  25590  volsuplem  25595  volsup  25596  dyadmax  25638  itgfsum  25867  dvnadd  25969  cpnord  25975  dvnfre  25992  dvmptfsum  26015  ply1divex  26175  fta1g  26208  plyco  26279  dgrcolem1  26311  dgrco  26313  dvnply2  26326  plydivex  26336  aaliou3lem2  26382  dvntaylp  26409  taylthlem1  26411  cxpmul2  26729  jensen  27028  ftalem2  27113  bcmono  27316  bposlem5  27327  lgsquad2lem2  27424  dchrisumlem1  27528  dchrisum0flb  27549  pntpbnd1  27625  pntlemf  27644  qabvle  27664  qabvexp  27665  ostthlem2  27667  ostth2lem2  27673  nosupbnd1lem5  27751  noinfbnd1lem5  27766  precsexlem8  28282  precsexlem9  28283  om2noseqrdg  28372  n0addscl  28412  n0mulscl  28413  eucliddivs  28444  peano5uzs  28472  expscllem  28498  expadds  28503  expsne0  28504  expsgt0  28505  pw2cut  28528  pw2cut2  28530  rusgrnumwwlk  30122  eupth2lems  30384  eupth2  30385  ipasslem1  30978  mdslmd1lem1  32472  mdslmd1lem2  32473  iuninc  32707  ssrelf  32765  nn0min  32971  nexple  32994  gsumwun  33215  gsumvsca1  33365  gsumvsca2  33366  domnprodn0  33418  unitprodclb  33534  1arithufdlem3  33701  cmppcmp  34114  esumfzf  34325  sseqp1  34651  rrvsum  34710  signstfvc  34830  bnj1174  35260  lfuhgr2  35422  subfacp1lem6  35488  mrsubvrs  35825  bccolsum  36042  iprodefisumlem  36043  faclimlem1  36046  onsuct0  36754  findfvcl  36765  poimirlem28  38100  sdclem2  38194  seqpo  38199  incsequz  38200  mettrifi  38209  heiborlem4  38266  bfplem1  38274  pclfinclN  40527  uzindd  42548  indstrd  42763  sn-sup2  43066  incssnn0  43245  mzpexpmpt  43279  pell14qrexpclnn0  43396  monotuz  43471  rmxypos  43477  jm2.17a  43490  jm2.17b  43491  rmygeid  43494  jm2.18  43518  jm2.19lem3  43521  jm2.15nn0  43533  jm2.16nn0  43534  dfac11  43592  pwslnm  43624  hbtlem5  43658  cnsrexpcl  43695  cantnfresb  43854  onmcl  43861  naddonnn  43925  relexpxpnnidm  44232  relexpiidm  44233  relexpss1d  44234  iunrelexpmin1  44237  relexpmulnn  44238  iunrelexpmin2  44241  relexp0a  44245  trclimalb2  44255  dvgrat  44841  relpfrlem  45482  trfr  45491  lmodvsmdi  48954  tfis2d  50254