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  846  minimp  1622  cbv1v  2338  cbv1  2404  ralimdva  3145  reuss2  4275  ssrel  5727  ssrel2  5729  ssrelrel  5740  funfvima2  7171  isofrlem  7280  dfwe2  7713  tfindsg  7797  tfinds2  7800  tfinds3  7801  trom  7811  findsg  7833  finds2  7834  xpord3inddlem  8090  fpr3g  8221  wfr3g  8255  tfrlem1  8301  tfr3  8324  tz7.48lem  8366  oaordi  8467  oeordi  8508  nnaordi  8539  nnawordi  8542  naddssim  8606  naddoa  8623  nneneq  9122  ac6sfi  9175  fodomfi  9203  domunfican  9213  fodomfiOLD  9221  finsschain  9250  marypha1lem  9324  inf3lem2  9526  inf3lem5  9529  cantnfval2  9566  cantnflt  9569  cantnfp1lem3  9577  cnfcom  9597  ttrclss  9617  ttrclselem2  9623  frr3g  9656  dfac12lem3  10044  ackbij1lem16  10132  sornom  10175  infpssrlem4  10204  fin23lem34  10244  fin23lem36  10246  isf32lem1  10251  isf32lem2  10252  zorn2lem4  10397  zorn2lem5  10398  zorn2lem6  10399  zorn2lem7  10400  ttukeylem5  10411  pwfseqlem3  10558  wunfi  10619  grudomon  10715  prlem934  10931  sup2  12085  nnindd  12152  nnaddcl  12155  nnmulcl  12156  nnne0  12166  peano5uzi  12568  uzind2  12572  nn0indd  12576  fzind  12577  zindd  12580  fzindd  12581  uzaddcl  12804  uzwo  12811  om2uzlti  13859  seqcaopr3  13946  seqf1olem2a  13949  seqf1o  13952  ser1const  13967  expcllem  13981  expeq0  14001  mulexp  14010  expadd  14013  expmul  14016  expmordi  14076  leexp2r  14083  leexp1a  14084  bernneq  14138  modexp  14147  facdiv  14196  facwordi  14198  faclbnd  14199  faclbnd4lem4  14205  hashgadd  14286  hashmap  14344  hashf1lem2  14365  hashf1  14366  seqcoll  14373  cshweqrep  14730  relexpsucnnl  14939  relexpcnv  14944  relexpnndm  14950  relexpaddnn  14960  rlimsqzlem  15558  lo1le  15561  iseraltlem2  15592  fsum2d  15680  modfsummod  15703  fsumabs  15710  fsumrlim  15720  fsumo1  15721  fsumiun  15730  binom  15739  climcndslem1  15758  climcndslem2  15759  cvgrat  15792  clim2prod  15797  prodfn0  15803  prodfrec  15804  ntrivcvgfvn0  15808  fprodabs  15883  fprod2d  15890  binomfallfac  15950  bpolycl  15961  fprodefsum  16004  demoivreALT  16112  ruclem8  16148  ruclem9  16149  dvdsfac  16239  bitsinv1  16355  sadcadd  16371  sadadd2  16373  saddisjlem  16377  smuval2  16395  smupvallem  16396  smu01lem  16398  smupval  16401  smueqlem  16403  smumullem  16405  rplpwr  16471  nn0seqcvgd  16483  seq1st  16484  alginv  16488  algcvga  16492  algfx  16493  prmdvdsexp  16628  prmfac1  16633  eulerthlem2  16695  pcmpt  16806  pcfac  16813  prmpwdvds  16818  prmreclem4  16833  vdwlem10  16904  ramcl  16943  mreexexd  17556  frmdgsum  18772  mulgnnass  19024  mhmmulg  19030  gsumwrev  19280  gsmsymgrfix  19342  gsmsymgreq  19346  efginvrel2  19641  efgsrel  19648  gsum2dlem2  19885  ablfac1eulem  19988  pgpfac  20000  gsumle  20059  srgmulgass  20137  srgpcomp  20138  srgbinom  20151  lmodvsmmulgdi  20832  cnfldexp  21343  ofldchr  21515  assamulgscm  21840  mplcoe1  21973  mplcoe3  21974  mplcoe5  21976  mptcoe1fsupp  22129  coe1fzgsumdlem  22219  coe1fzgsumd  22220  gsummoncoe1  22224  evl1gsumdlem  22272  evl1gsumd  22273  mdetunilem9  22536  mptcoe1matfsupp  22718  mp2pm2mplem4  22725  chpdmat  22757  tgcl  22885  fiuncmp  23320  2ndcsep  23375  1stcelcls  23377  ptcmpfi  23729  tmdgsum  24011  fsumcn  24789  caubl  25236  caublcls  25237  ovolunlem1a  25425  ovolfiniun  25430  volfiniun  25476  voliunlem1  25479  volsuplem  25484  volsup  25485  dyadmax  25527  itgfsum  25756  dvnadd  25859  cpnord  25865  dvnfre  25884  dvmptfsum  25907  ply1divex  26070  fta1g  26103  plyco  26174  dgrcolem1  26207  dgrco  26209  dvnply2  26223  plydivex  26233  aaliou3lem2  26279  dvntaylp  26307  taylthlem1  26309  cxpmul2  26626  jensen  26927  ftalem2  27012  bcmono  27216  bposlem5  27227  lgsquad2lem2  27324  dchrisumlem1  27428  dchrisum0flb  27449  pntpbnd1  27525  pntlemf  27544  qabvle  27564  qabvexp  27565  ostthlem2  27567  ostth2lem2  27573  nosupbnd1lem5  27652  noinfbnd1lem5  27667  precsexlem8  28153  precsexlem9  28154  om2noseqrdg  28235  n0addscl  28273  n0mulscl  28274  eucliddivs  28302  peano5uzs  28329  expscllem  28354  expadds  28359  expsne0  28360  expsgt0  28361  pw2cut  28381  pw2cut2  28383  rusgrnumwwlk  29958  eupth2lems  30220  eupth2  30221  ipasslem1  30813  mdslmd1lem1  32307  mdslmd1lem2  32308  iuninc  32542  ssrelf  32600  nn0min  32808  nexple  32832  gsumwun  33052  gsumvsca1  33202  gsumvsca2  33203  domnprodn0  33249  unitprodclb  33361  1arithufdlem3  33518  cmppcmp  33892  esumfzf  34103  sseqp1  34429  rrvsum  34488  signstfvc  34608  bnj1174  35036  lfuhgr2  35184  subfacp1lem6  35250  mrsubvrs  35587  bccolsum  35804  iprodefisumlem  35805  faclimlem1  35808  onsuct0  36506  findfvcl  36517  poimirlem28  37708  sdclem2  37802  seqpo  37807  incsequz  37808  mettrifi  37817  heiborlem4  37874  bfplem1  37882  pclfinclN  40069  uzindd  42090  indstrd  42306  nnaddcom  42386  nnadddir  42388  nnmulcom  42390  sn-sup2  42609  incssnn0  42828  mzpexpmpt  42862  pell14qrexpclnn0  42983  monotuz  43058  rmxypos  43064  jm2.17a  43077  jm2.17b  43078  rmygeid  43081  jm2.18  43105  jm2.19lem3  43108  jm2.15nn0  43120  jm2.16nn0  43121  dfac11  43179  pwslnm  43211  hbtlem5  43245  cnsrexpcl  43282  cantnfresb  43441  onmcl  43448  naddonnn  43512  relexpxpnnidm  43820  relexpiidm  43821  relexpss1d  43822  iunrelexpmin1  43825  relexpmulnn  43826  iunrelexpmin2  43829  relexp0a  43833  trclimalb2  43843  dvgrat  44429  relpfrlem  45070  trfr  45079  lmodvsmdi  48503  tfis2d  49805