Theorem a2d 30

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 18	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpdd  44  imim2d  58  imim3i  65  loowoz  113  animpimp2impd  860  minimp  1654  cbv1v  2366  cbv1  2432  ralimdva  3175  reuss2  4272  ssrel  5759  ssrel2  5761  ssrelrel  5772  funfvima2  7229  isofrlem  7340  dfwe2  7777  tfindsg  7861  tfinds2  7864  tfinds3  7865  trom  7875  findsg  7898  finds2  7899  xpord3inddlem  8155  fpr3g  8287  wfr3g  8321  tfrlem1  8367  tfr3  8391  tz7.48lemOLD  8435  oaordi  8538  oeordi  8580  nnaordi  8611  nnawordi  8614  naddssim  8679  naddoa  8696  nneneq  9205  ac6sfi  9259  fodomfi  9288  domunfican  9297  finsschain  9332  marypha1lem  9409  inf3lem2  9614  inf3lem5  9617  cantnfval2  9654  cantnflt  9657  cantnfp1lem3  9665  cnfcom  9685  ttrclss  9705  ttrclselem2  9711  frr3g  9744  dfac12lem3  10205  ackbij1lem16  10293  sornom  10336  infpssrlem4  10365  fin23lem34  10405  fin23lem36  10407  isf32lem1  10412  isf32lem2  10413  zorn2lem4  10558  zorn2lem5  10559  zorn2lem6  10560  zorn2lem7  10561  ttukeylem5  10572  pwfseqlem3  10726  wunfi  10787  grudomon  10883  prlem934  11099  sup2  12254  nnindd  12336  nnaddcl  12339  nnmulcl  12340  nnaddcom  12343  nnne0  12353  nnadddir  12375  nnmulcom  12377  peano5uzi  12769  uzind2  12773  nn0indd  12777  fzind  12778  zindd  12781  fzindd  12782  uzaddcl  13012  uzwo  13019  om2uzlti  14073  seqcaopr3  14160  seqf1olem2a  14163  seqf1o  14166  ser1const  14181  expcllem  14195  expeq0  14215  mulexp  14224  expadd  14227  expmul  14230  expmordi  14290  leexp2r  14297  leexp1a  14298  bernneq  14353  modexp  14362  facdiv  14411  facwordi  14413  faclbnd  14414  faclbnd4lem4  14420  hashgadd  14501  hashmap  14560  hashf1lem2  14581  hashf1  14582  seqcoll  14589  cshweqrep  14952  relexpsucnnl  15163  relexpcnv  15168  relexpnndm  15174  relexpaddnn  15184  rlimsqzlem  15796  lo1le  15799  iseraltlem2  15830  fsum2d  15917  modfsummod  15941  fsumabs  15948  fsumrlim  15958  fsumo1  15959  fsumiun  15968  binom  15979  climcndslem1  15998  climcndslem2  15999  cvgrat  16032  clim2prod  16037  prodfn0  16043  prodfrec  16044  ntrivcvgfvn0  16048  fprodabs  16121  fprod2d  16128  binomfallfac  16187  bpolycl  16198  fprodefsum  16241  demoivreALT  16349  ruclem8  16385  ruclem9  16386  dvdsfac  16476  bitsinv1  16592  sadcadd  16608  sadadd2  16610  saddisjlem  16614  smuval2  16632  smupvallem  16633  smu01lem  16635  smupval  16638  smueqlem  16640  smumullem  16642  rplpwr  16712  nn0seqcvgd  16725  seq1st  16726  alginv  16730  algcvga  16734  algfx  16735  prmdvdsexp  16871  prmfac1  16876  eulerthlem2  16939  pcmpt  17050  pcfac  17057  prmpwdvds  17062  prmreclem4  17077  vdwlem10  17148  ramcl  17187  mreexexd  17802  frmdgsum  19038  mulgnnass  19299  mhmmulg  19305  gsumwrev  19560  gsmsymgrfix  19622  gsmsymgreq  19626  efginvrel2  19921  efgsrel  19928  gsum2dlem2  20165  ablfac1eulem  20268  pgpfac  20280  gsumle  20339  srgmulgass  20423  srgpcomp  20424  srgbinom  20437  lmodvsmmulgdi  21152  cnfldexp  21691  ofldchr  21862  assamulgscm  22189  mplcoe1  22326  mplcoe3  22327  mplcoe5  22329  mptcoe1fsupp  22513  coe1fzgsumdlem  22601  coe1fzgsumd  22602  gsummoncoe1  22606  evl1gsumdlem  22654  evl1gsumd  22655  mdetunilem9  22915  mptcoe1matfsupp  23100  mp2pm2mplem4  23107  chpdmat  23139  tgcl  23267  fiuncmp  23702  2ndcsep  23758  1stcelcls  23760  ptcmpfi  24112  tmdgsum  24394  fsumcn  25171  caubl  25609  caublcls  25610  ovolunlem1a  25797  ovolfiniun  25802  volfiniun  25848  voliunlem1  25851  volsuplem  25856  volsup  25857  dyadmax  25899  itgfsum  26127  dvnadd  26229  cpnord  26235  dvnfre  26252  dvmptfsum  26275  ply1divex  26435  fta1g  26468  plyco  26540  dgrcolem1  26572  dgrco  26574  dvnply2  26590  plydivex  26600  aaliou3lem2  26652  dvntaylp  26680  taylthlem1  26682  cxpmul2  26999  jensen  27298  ftalem2  27383  bcmono  27586  bposlem5  27597  lgsquad2lem2  27694  dchrisumlem1  27798  dchrisum0flb  27819  pntpbnd1  27895  pntlemf  27914  qabvle  27934  qabvexp  27935  ostthlem2  27937  ostth2lem2  27943  nosupbnd1lem5  28051  noinfbnd1lem5  28066  precsexlem8  28582  precsexlem9  28583  om2noseqrdg  28672  n0addscl  28712  n0mulscl  28713  eucliddivs  28744  peano5uzs  28772  expscllem  28798  expadds  28803  expsne0  28804  expsgt0  28805  pw2cut  28828  pw2cut2  28830  plngrotlem2  29248  lfuhgr2  29709  rusgrnumwwlk  30549  eupth2lems  30821  eupth2  30822  ipasslem1  31415  mdslmd1lem1  32909  mdslmd1lem2  32910  iuninc  33137  ssrelf  33191  nn0min  33394  nexple  33406  gsumwun  33619  gsumvsca1  33769  gsumvsca2  33770  domnprodn0  33821  unitprodclb  33926  1arithufdlem3  34060  cmppcmp  34472  esumfzf  34683  sseqp1  35010  rrvsum  35069  signstfvc  35186  bnj1174  35616  subfacp1lem6  35919  mrsubvrs  36256  bccolsum  36473  iprodefisumlem  36474  faclimlem1  36477  onsuct0  37199  findfvcl  37210  poimirlem28  38534  sdclem2  38644  seqpo  38649  incsequz  38650  mettrifi  38659  heiborlem4  38716  bfplem1  38724  pclfinclN  40975  uzindd  42996  indstrd  43211  sn-sup2  43523  incssnn0  43675  mzpexpmpt  43709  pell14qrexpclnn0  43826  monotuz  43901  rmxypos  43907  jm2.17a  43920  jm2.17b  43921  rmygeid  43924  jm2.18  43948  jm2.19lem3  43951  jm2.15nn0  43963  jm2.16nn0  43964  dfac11  44022  pwslnm  44054  hbtlem5  44088  cnsrexpcl  44125  cantnfresb  44284  onmcl  44291  naddonnn  44355  relexpxpnnidm  44662  relexpiidm  44663  relexpss1d  44664  iunrelexpmin1  44667  relexpmulnn  44668  iunrelexpmin2  44671  relexp0a  44675  trclimalb2  44685  dvgrat  45255  relpfrlem  45895  trfr  45904  lmodvsmdi  49435  tfis2d  50731