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  1618  cbv1v  2337  cbv1  2405  ralimdva  3165  reuss2  4332  ssrel  5795  ssrelOLD  5796  ssrel2  5798  ssrelrel  5809  funfvima2  7251  isofrlem  7360  dfwe2  7793  tfindsg  7882  tfinds2  7885  tfinds3  7886  trom  7896  findsg  7920  finds2  7921  xpord3inddlem  8178  fpr3g  8309  wfr3g  8346  tfrlem1  8415  tfr3  8438  tz7.48lem  8480  oaordi  8583  oeordi  8624  nnaordi  8655  nnawordi  8658  naddssim  8722  naddoa  8739  nneneq  9244  nneneqOLD  9256  ac6sfi  9318  fodomfi  9348  domunfican  9359  fodomfiOLD  9368  finsschain  9397  marypha1lem  9471  inf3lem2  9667  inf3lem5  9670  cantnfval2  9707  cantnflt  9710  cantnfp1lem3  9718  cnfcom  9738  ttrclss  9758  ttrclselem2  9764  frr3g  9794  dfac12lem3  10184  ackbij1lem16  10272  sornom  10315  infpssrlem4  10344  fin23lem34  10384  fin23lem36  10386  isf32lem1  10391  isf32lem2  10392  zorn2lem4  10537  zorn2lem5  10538  zorn2lem6  10539  zorn2lem7  10540  ttukeylem5  10551  pwfseqlem3  10698  wunfi  10759  grudomon  10855  prlem934  11071  sup2  12222  nnindd  12284  nnaddcl  12287  nnmulcl  12288  nnne0  12298  peano5uzi  12705  uzind2  12709  nn0indd  12713  fzind  12714  zindd  12717  fzindd  12718  uzaddcl  12944  uzwo  12951  om2uzlti  13988  seqcaopr3  14075  seqf1olem2a  14078  seqf1o  14081  ser1const  14096  expcllem  14110  expeq0  14130  mulexp  14139  expadd  14142  expmul  14145  expmordi  14204  leexp2r  14211  leexp1a  14212  bernneq  14265  modexp  14274  facdiv  14323  facwordi  14325  faclbnd  14326  faclbnd4lem4  14332  hashgadd  14413  hashmap  14471  hashf1lem2  14492  hashf1  14493  seqcoll  14500  cshweqrep  14856  relexpsucnnl  15066  relexpcnv  15071  relexpnndm  15077  relexpaddnn  15087  rlimsqzlem  15682  lo1le  15685  iseraltlem2  15716  fsum2d  15804  modfsummod  15827  fsumabs  15834  fsumrlim  15844  fsumo1  15845  fsumiun  15854  binom  15863  climcndslem1  15882  climcndslem2  15883  cvgrat  15916  clim2prod  15921  prodfn0  15927  prodfrec  15928  ntrivcvgfvn0  15932  fprodabs  16007  fprod2d  16014  binomfallfac  16074  bpolycl  16085  fprodefsum  16128  demoivreALT  16234  ruclem8  16270  ruclem9  16271  dvdsfac  16360  bitsinv1  16476  sadcadd  16492  sadadd2  16494  saddisjlem  16498  smuval2  16516  smupvallem  16517  smu01lem  16519  smupval  16522  smueqlem  16524  smumullem  16526  rplpwr  16592  nn0seqcvgd  16604  seq1st  16605  alginv  16609  algcvga  16613  algfx  16614  prmdvdsexp  16749  prmfac1  16754  eulerthlem2  16816  pcmpt  16926  pcfac  16933  prmpwdvds  16938  prmreclem4  16953  vdwlem10  17024  ramcl  17063  mreexexd  17693  frmdgsum  18888  mulgnnass  19140  mhmmulg  19146  gsumwrev  19400  gsmsymgrfix  19461  gsmsymgreq  19465  efginvrel2  19760  efgsrel  19767  gsum2dlem2  20004  ablfac1eulem  20107  pgpfac  20119  srgmulgass  20235  srgpcomp  20236  srgbinom  20249  lmodvsmmulgdi  20912  cnfldexp  21435  assamulgscm  21939  mplcoe1  22073  mplcoe3  22074  mplcoe5  22076  mptcoe1fsupp  22233  coe1fzgsumdlem  22323  coe1fzgsumd  22324  gsummoncoe1  22328  evl1gsumdlem  22376  evl1gsumd  22377  mdetunilem9  22642  mptcoe1matfsupp  22824  mp2pm2mplem4  22831  chpdmat  22863  tgcl  22992  fiuncmp  23428  2ndcsep  23483  1stcelcls  23485  ptcmpfi  23837  tmdgsum  24119  fsumcn  24908  caubl  25356  caublcls  25357  ovolunlem1a  25545  ovolfiniun  25550  volfiniun  25596  voliunlem1  25599  volsuplem  25604  volsup  25605  dyadmax  25647  itgfsum  25877  dvnadd  25980  cpnord  25986  dvnfre  26005  dvmptfsum  26028  ply1divex  26191  fta1g  26224  plyco  26295  dgrcolem1  26328  dgrco  26330  dvnply2  26344  plydivex  26354  aaliou3lem2  26400  dvntaylp  26428  taylthlem1  26430  cxpmul2  26746  jensen  27047  ftalem2  27132  bcmono  27336  bposlem5  27347  lgsquad2lem2  27444  dchrisumlem1  27548  dchrisum0flb  27569  pntpbnd1  27645  pntlemf  27664  qabvle  27684  qabvexp  27685  ostthlem2  27687  ostth2lem2  27693  nosupbnd1lem5  27772  noinfbnd1lem5  27787  precsexlem8  28253  precsexlem9  28254  om2noseqrdg  28325  n0addscl  28362  n0mulscl  28363  peano5uzs  28405  expscl  28428  expsne0  28429  expsgt0  28430  pw2cut  28435  rusgrnumwwlk  30005  eupth2lems  30267  eupth2  30268  ipasslem1  30860  mdslmd1lem1  32354  mdslmd1lem2  32355  iuninc  32581  ssrelf  32635  nn0min  32827  gsumwun  33051  gsumle  33084  gsumvsca1  33215  gsumvsca2  33216  domnprodn0  33262  ofldchr  33324  unitprodclb  33397  1arithufdlem3  33554  cmppcmp  33819  nexple  33990  esumfzf  34050  sseqp1  34377  rrvsum  34436  signstfvc  34568  bnj1174  34996  lfuhgr2  35103  subfacp1lem6  35170  mrsubvrs  35507  bccolsum  35719  iprodefisumlem  35720  faclimlem1  35723  onsuct0  36424  findfvcl  36435  poimirlem28  37635  sdclem2  37729  seqpo  37734  incsequz  37735  mettrifi  37744  heiborlem4  37801  bfplem1  37809  pclfinclN  39933  uzindd  41959  indstrd  42175  nnaddcom  42282  nnadddir  42284  nnmulcom  42286  sn-sup2  42478  incssnn0  42699  mzpexpmpt  42733  pell14qrexpclnn0  42854  monotuz  42930  rmxypos  42936  jm2.17a  42949  jm2.17b  42950  rmygeid  42953  jm2.18  42977  jm2.19lem3  42980  jm2.15nn0  42992  jm2.16nn0  42993  dfac11  43051  pwslnm  43083  hbtlem5  43117  cnsrexpcl  43154  cantnfresb  43314  onmcl  43321  naddonnn  43385  relexpxpnnidm  43693  relexpiidm  43694  relexpss1d  43695  iunrelexpmin1  43698  relexpmulnn  43699  iunrelexpmin2  43702  relexp0a  43706  trclimalb2  43716  dvgrat  44308  lmodvsmdi  48224  tfis2d  48911