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  1621  cbv1v  2334  cbv1  2401  ralimdva  3146  reuss2  4292  ssrel  5748  ssrelOLD  5749  ssrel2  5751  ssrelrel  5762  funfvima2  7208  isofrlem  7318  dfwe2  7753  tfindsg  7840  tfinds2  7843  tfinds3  7844  trom  7854  findsg  7876  finds2  7877  xpord3inddlem  8136  fpr3g  8267  wfr3g  8301  tfrlem1  8347  tfr3  8370  tz7.48lem  8412  oaordi  8513  oeordi  8554  nnaordi  8585  nnawordi  8588  naddssim  8652  naddoa  8669  nneneq  9176  ac6sfi  9238  fodomfi  9268  domunfican  9279  fodomfiOLD  9288  finsschain  9317  marypha1lem  9391  inf3lem2  9589  inf3lem5  9592  cantnfval2  9629  cantnflt  9632  cantnfp1lem3  9640  cnfcom  9660  ttrclss  9680  ttrclselem2  9686  frr3g  9716  dfac12lem3  10106  ackbij1lem16  10194  sornom  10237  infpssrlem4  10266  fin23lem34  10306  fin23lem36  10308  isf32lem1  10313  isf32lem2  10314  zorn2lem4  10459  zorn2lem5  10460  zorn2lem6  10461  zorn2lem7  10462  ttukeylem5  10473  pwfseqlem3  10620  wunfi  10681  grudomon  10777  prlem934  10993  sup2  12146  nnindd  12213  nnaddcl  12216  nnmulcl  12217  nnne0  12227  peano5uzi  12630  uzind2  12634  nn0indd  12638  fzind  12639  zindd  12642  fzindd  12643  uzaddcl  12870  uzwo  12877  om2uzlti  13922  seqcaopr3  14009  seqf1olem2a  14012  seqf1o  14015  ser1const  14030  expcllem  14044  expeq0  14064  mulexp  14073  expadd  14076  expmul  14079  expmordi  14139  leexp2r  14146  leexp1a  14147  bernneq  14201  modexp  14210  facdiv  14259  facwordi  14261  faclbnd  14262  faclbnd4lem4  14268  hashgadd  14349  hashmap  14407  hashf1lem2  14428  hashf1  14429  seqcoll  14436  cshweqrep  14793  relexpsucnnl  15003  relexpcnv  15008  relexpnndm  15014  relexpaddnn  15024  rlimsqzlem  15622  lo1le  15625  iseraltlem2  15656  fsum2d  15744  modfsummod  15767  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fsumiun  15794  binom  15803  climcndslem1  15822  climcndslem2  15823  cvgrat  15856  clim2prod  15861  prodfn0  15867  prodfrec  15868  ntrivcvgfvn0  15872  fprodabs  15947  fprod2d  15954  binomfallfac  16014  bpolycl  16025  fprodefsum  16068  demoivreALT  16176  ruclem8  16212  ruclem9  16213  dvdsfac  16303  bitsinv1  16419  sadcadd  16435  sadadd2  16437  saddisjlem  16441  smuval2  16459  smupvallem  16460  smu01lem  16462  smupval  16465  smueqlem  16467  smumullem  16469  rplpwr  16535  nn0seqcvgd  16547  seq1st  16548  alginv  16552  algcvga  16556  algfx  16557  prmdvdsexp  16692  prmfac1  16697  eulerthlem2  16759  pcmpt  16870  pcfac  16877  prmpwdvds  16882  prmreclem4  16897  vdwlem10  16968  ramcl  17007  mreexexd  17616  frmdgsum  18796  mulgnnass  19048  mhmmulg  19054  gsumwrev  19305  gsmsymgrfix  19365  gsmsymgreq  19369  efginvrel2  19664  efgsrel  19671  gsum2dlem2  19908  ablfac1eulem  20011  pgpfac  20023  srgmulgass  20133  srgpcomp  20134  srgbinom  20147  lmodvsmmulgdi  20810  cnfldexp  21323  assamulgscm  21817  mplcoe1  21951  mplcoe3  21952  mplcoe5  21954  mptcoe1fsupp  22107  coe1fzgsumdlem  22197  coe1fzgsumd  22198  gsummoncoe1  22202  evl1gsumdlem  22250  evl1gsumd  22251  mdetunilem9  22514  mptcoe1matfsupp  22696  mp2pm2mplem4  22703  chpdmat  22735  tgcl  22863  fiuncmp  23298  2ndcsep  23353  1stcelcls  23355  ptcmpfi  23707  tmdgsum  23989  fsumcn  24768  caubl  25215  caublcls  25216  ovolunlem1a  25404  ovolfiniun  25409  volfiniun  25455  voliunlem1  25458  volsuplem  25463  volsup  25464  dyadmax  25506  itgfsum  25735  dvnadd  25838  cpnord  25844  dvnfre  25863  dvmptfsum  25886  ply1divex  26049  fta1g  26082  plyco  26153  dgrcolem1  26186  dgrco  26188  dvnply2  26202  plydivex  26212  aaliou3lem2  26258  dvntaylp  26286  taylthlem1  26288  cxpmul2  26605  jensen  26906  ftalem2  26991  bcmono  27195  bposlem5  27206  lgsquad2lem2  27303  dchrisumlem1  27407  dchrisum0flb  27428  pntpbnd1  27504  pntlemf  27523  qabvle  27543  qabvexp  27544  ostthlem2  27546  ostth2lem2  27552  nosupbnd1lem5  27631  noinfbnd1lem5  27646  precsexlem8  28123  precsexlem9  28124  om2noseqrdg  28205  n0addscl  28243  n0mulscl  28244  eucliddivs  28272  peano5uzs  28299  expscllem  28323  expadds  28327  expsne0  28328  expsgt0  28329  pw2cut  28342  rusgrnumwwlk  29912  eupth2lems  30174  eupth2  30175  ipasslem1  30767  mdslmd1lem1  32261  mdslmd1lem2  32262  iuninc  32496  ssrelf  32550  nn0min  32752  nexple  32776  gsumwun  33012  gsumle  33045  gsumvsca1  33186  gsumvsca2  33187  domnprodn0  33233  ofldchr  33299  unitprodclb  33367  1arithufdlem3  33524  cmppcmp  33855  esumfzf  34066  sseqp1  34393  rrvsum  34452  signstfvc  34572  bnj1174  35000  lfuhgr2  35113  subfacp1lem6  35179  mrsubvrs  35516  bccolsum  35733  iprodefisumlem  35734  faclimlem1  35737  onsuct0  36436  findfvcl  36447  poimirlem28  37649  sdclem2  37743  seqpo  37748  incsequz  37749  mettrifi  37758  heiborlem4  37815  bfplem1  37823  pclfinclN  39951  uzindd  41972  indstrd  42188  nnaddcom  42263  nnadddir  42265  nnmulcom  42267  sn-sup2  42486  incssnn0  42706  mzpexpmpt  42740  pell14qrexpclnn0  42861  monotuz  42937  rmxypos  42943  jm2.17a  42956  jm2.17b  42957  rmygeid  42960  jm2.18  42984  jm2.19lem3  42987  jm2.15nn0  42999  jm2.16nn0  43000  dfac11  43058  pwslnm  43090  hbtlem5  43124  cnsrexpcl  43161  cantnfresb  43320  onmcl  43327  naddonnn  43391  relexpxpnnidm  43699  relexpiidm  43700  relexpss1d  43701  iunrelexpmin1  43704  relexpmulnn  43705  iunrelexpmin2  43708  relexp0a  43712  trclimalb2  43722  dvgrat  44308  relpfrlem  44950  trfr  44959  lmodvsmdi  48371  tfis2d  49673