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  843  minimp  1622  cbv1v  2332  cbv1  2400  ralimdva  3160  reuss2  4262  ssrel  5724  ssrelOLD  5725  ssrel2  5727  ssrelrel  5738  funfvima2  7163  isofrlem  7267  dfwe2  7686  tfindsg  7775  tfinds2  7778  tfinds3  7779  trom  7789  findsg  7814  finds2  7815  fpr3g  8171  wfr3g  8208  tfrlem1  8277  tfr3  8300  tz7.48lem  8342  oaordi  8448  oeordi  8489  nnaordi  8520  nnawordi  8523  nneneq  9074  nneneqOLD  9086  ac6sfi  9152  domunfican  9185  fodomfi  9190  finsschain  9224  marypha1lem  9290  inf3lem2  9486  inf3lem5  9489  cantnfval2  9526  cantnflt  9529  cantnfp1lem3  9537  cnfcom  9557  ttrclss  9577  ttrclselem2  9583  frr3g  9613  dfac12lem3  10002  ackbij1lem16  10092  sornom  10134  infpssrlem4  10163  fin23lem34  10203  fin23lem36  10205  isf32lem1  10210  isf32lem2  10211  zorn2lem4  10356  zorn2lem5  10357  zorn2lem6  10358  zorn2lem7  10359  ttukeylem5  10370  pwfseqlem3  10517  wunfi  10578  grudomon  10674  prlem934  10890  sup2  12032  nnindd  12094  nnaddcl  12097  nnmulcl  12098  nnne0  12108  peano5uzi  12510  uzind2  12514  nn0indd  12518  fzind  12519  zindd  12522  fzindd  12523  uzaddcl  12745  uzwo  12752  om2uzlti  13771  seqcaopr3  13859  seqf1olem2a  13862  seqf1o  13865  ser1const  13880  expcllem  13894  expeq0  13914  mulexp  13923  expadd  13926  expmul  13929  expmordi  13986  leexp2r  13993  leexp1a  13994  bernneq  14045  modexp  14054  facdiv  14102  facwordi  14104  faclbnd  14105  faclbnd4lem4  14111  hashgadd  14192  hashmap  14250  hashf1lem2  14270  hashf1  14271  seqcoll  14278  cshweqrep  14632  relexpsucnnl  14840  relexpcnv  14845  relexpnndm  14851  relexpaddnn  14861  rlimsqzlem  15459  lo1le  15462  iseraltlem2  15493  fsum2d  15582  modfsummod  15605  fsumabs  15612  fsumrlim  15622  fsumo1  15623  fsumiun  15632  binom  15641  climcndslem1  15660  climcndslem2  15661  cvgrat  15694  clim2prod  15699  prodfn0  15705  prodfrec  15706  ntrivcvgfvn0  15710  fprodabs  15783  fprod2d  15790  binomfallfac  15850  bpolycl  15861  fprodefsum  15903  demoivreALT  16009  ruclem8  16045  ruclem9  16046  dvdsfac  16134  bitsinv1  16248  sadcadd  16264  sadadd2  16266  saddisjlem  16270  smuval2  16288  smupvallem  16289  smu01lem  16291  smupval  16294  smueqlem  16296  smumullem  16298  rplpwr  16364  nn0seqcvgd  16372  seq1st  16373  alginv  16377  algcvga  16381  algfx  16382  prmdvdsexp  16517  prmfac1  16523  eulerthlem2  16580  pcmpt  16690  pcfac  16697  prmpwdvds  16702  prmreclem4  16717  vdwlem10  16788  ramcl  16827  mreexexd  17454  frmdgsum  18597  mulgnnass  18834  mhmmulg  18840  gsumwrev  19069  gsmsymgrfix  19132  gsmsymgreq  19136  efginvrel2  19428  efgsrel  19435  gsum2dlem2  19667  ablfac1eulem  19770  pgpfac  19782  srgmulgass  19862  srgpcomp  19863  srgbinom  19876  lmodvsmmulgdi  20264  cnfldexp  20737  assamulgscm  21211  mplcoe1  21344  mplcoe3  21345  mplcoe5  21347  mptcoe1fsupp  21492  coe1fzgsumdlem  21578  coe1fzgsumd  21579  gsummoncoe1  21581  evl1gsumdlem  21628  evl1gsumd  21629  mdetunilem9  21875  mptcoe1matfsupp  22057  mp2pm2mplem4  22064  chpdmat  22096  tgcl  22225  fiuncmp  22661  2ndcsep  22716  1stcelcls  22718  ptcmpfi  23070  tmdgsum  23352  fsumcn  24139  caubl  24578  caublcls  24579  ovolunlem1a  24766  ovolfiniun  24771  volfiniun  24817  voliunlem1  24820  volsuplem  24825  volsup  24826  dyadmax  24868  itgfsum  25097  dvnadd  25199  cpnord  25205  dvnfre  25222  dvmptfsum  25245  ply1divex  25407  fta1g  25438  plyco  25508  dgrcolem1  25540  dgrco  25542  dvnply2  25553  plydivex  25563  aaliou3lem2  25609  dvntaylp  25636  taylthlem1  25638  cxpmul2  25950  jensen  26244  ftalem2  26329  bcmono  26531  bposlem5  26542  lgsquad2lem2  26639  dchrisumlem1  26743  dchrisum0flb  26764  pntpbnd1  26840  pntlemf  26859  qabvle  26879  qabvexp  26880  ostthlem2  26882  ostth2lem2  26888  nosupbnd1lem5  26966  noinfbnd1lem5  26981  rusgrnumwwlk  28628  eupth2lems  28890  eupth2  28891  ipasslem1  29481  mdslmd1lem1  30975  mdslmd1lem2  30976  iuninc  31187  ssrelf  31242  nn0min  31421  gsumle  31637  gsumvsca1  31766  gsumvsca2  31767  ofldchr  31813  cmppcmp  32106  nexple  32275  esumfzf  32335  sseqp1  32662  rrvsum  32721  signstfvc  32853  bnj1174  33282  lfuhgr2  33379  subfacp1lem6  33446  mrsubvrs  33783  bccolsum  33995  iprodefisumlem  33996  faclimlem1  33999  naddssim  34116  onsuct0  34726  findfvcl  34737  poimirlem28  35918  sdclem2  36013  seqpo  36018  incsequz  36019  mettrifi  36028  heiborlem4  36085  bfplem1  36093  pclfinclN  38226  uzindd  40247  nnaddcom  40566  nnadddir  40568  nnmulcom  40570  sn-sup2  40707  incssnn0  40803  mzpexpmpt  40837  pell14qrexpclnn0  40958  monotuz  41034  rmxypos  41040  jm2.17a  41053  jm2.17b  41054  rmygeid  41057  jm2.18  41081  jm2.19lem3  41084  jm2.15nn0  41096  jm2.16nn0  41097  dfac11  41158  pwslnm  41190  hbtlem5  41224  cnsrexpcl  41261  relexpxpnnidm  41641  relexpiidm  41642  relexpss1d  41643  iunrelexpmin1  41646  relexpmulnn  41647  iunrelexpmin2  41650  relexp0a  41654  trclimalb2  41664  dvgrat  42260  lmodvsmdi  46078  tfis2d  46746