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  1653  cbv1v  2365  cbv1  2431  ralimdva  3174  reuss2  4271  ssrel  5758  ssrel2  5760  ssrelrel  5771  funfvima2  7237  isofrlem  7348  dfwe2  7788  tfindsg  7872  tfinds2  7875  tfinds3  7876  trom  7886  findsg  7909  finds2  7910  xpord3inddlem  8173  fpr3g  8306  wfr3g  8340  tfrlem1  8386  tfr3  8410  tz7.48lemOLD  8454  oaordi  8557  oeordi  8599  nnaordi  8630  nnawordi  8633  naddssim  8698  naddoa  8715  nneneq  9224  ac6sfi  9278  fodomfi  9307  domunfican  9316  finsschain  9351  marypha1lem  9428  inf3lem2  9633  inf3lem5  9636  cantnfval2  9673  cantnflt  9676  cantnfp1lem3  9684  cnfcom  9704  ttrclss  9724  ttrclselem2  9730  frr3g  9763  dfac12lem3  10227  ackbij1lem16  10315  sornom  10358  infpssrlem4  10387  fin23lem34  10427  fin23lem36  10429  isf32lem1  10434  isf32lem2  10435  zorn2lem4  10580  zorn2lem5  10581  zorn2lem6  10582  zorn2lem7  10583  ttukeylem5  10594  pwfseqlem3  10748  wunfi  10809  grudomon  10905  prlem934  11121  sup2  12276  nnindd  12358  nnaddcl  12361  nnmulcl  12362  nnaddcom  12365  nnne0  12375  nnadddir  12397  nnmulcom  12399  peano5uzi  12791  uzind2  12795  nn0indd  12799  fzind  12800  zindd  12803  fzindd  12804  uzaddcl  13034  uzwo  13041  om2uzlti  14096  seqcaopr3  14183  seqf1olem2a  14186  seqf1o  14189  ser1const  14204  expcllem  14218  expeq0  14238  mulexp  14247  expadd  14250  expmul  14253  expmordi  14313  leexp2r  14320  leexp1a  14321  bernneq  14376  modexp  14385  facdiv  14434  facwordi  14436  faclbnd  14437  faclbnd4lem4  14443  hashgadd  14524  hashmap  14583  hashf1lem2  14604  hashf1  14605  seqcoll  14612  cshweqrep  14976  relexpsucnnl  15188  relexpcnv  15193  relexpnndm  15199  relexpaddnn  15209  rlimsqzlem  15821  lo1le  15824  iseraltlem2  15855  fsum2d  15942  modfsummod  15966  fsumabs  15973  fsumrlim  15983  fsumo1  15984  fsumiun  15993  binom  16004  climcndslem1  16023  climcndslem2  16024  cvgrat  16057  clim2prod  16062  prodfn0  16068  prodfrec  16069  ntrivcvgfvn0  16073  fprodabs  16146  fprod2d  16153  binomfallfac  16212  bpolycl  16223  fprodefsum  16266  demoivreALT  16374  ruclem8  16410  ruclem9  16411  dvdsfac  16501  bitsinv1  16617  sadcadd  16633  sadadd2  16635  saddisjlem  16639  smuval2  16657  smupvallem  16658  smu01lem  16660  smupval  16663  smueqlem  16665  smumullem  16667  rplpwr  16737  nn0seqcvgd  16750  seq1st  16751  alginv  16755  algcvga  16759  algfx  16760  prmdvdsexp  16896  prmfac1  16901  eulerthlem2  16964  pcmpt  17075  pcfac  17082  prmpwdvds  17087  prmreclem4  17102  vdwlem10  17173  ramcl  17212  mreexexd  17827  frmdgsum  19063  mulgnnass  19324  mhmmulg  19330  gsumwrev  19585  gsmsymgrfix  19647  gsmsymgreq  19651  efginvrel2  19946  efgsrel  19953  gsum2dlem2  20190  ablfac1eulem  20293  pgpfac  20305  gsumle  20364  srgmulgass  20448  srgpcomp  20449  srgbinom  20462  lmodvsmmulgdi  21177  cnfldexp  21716  ofldchr  21887  assamulgscm  22214  mplcoe1  22351  mplcoe3  22352  mplcoe5  22354  mptcoe1fsupp  22538  coe1fzgsumdlem  22626  coe1fzgsumd  22627  gsummoncoe1  22631  evl1gsumdlem  22679  evl1gsumd  22680  mdetunilem9  22940  mptcoe1matfsupp  23125  mp2pm2mplem4  23132  chpdmat  23164  tgcl  23292  fiuncmp  23727  2ndcsep  23783  1stcelcls  23785  ptcmpfi  24137  tmdgsum  24419  fsumcn  25196  caubl  25634  caublcls  25635  ovolunlem1a  25822  ovolfiniun  25827  volfiniun  25873  voliunlem1  25876  volsuplem  25881  volsup  25882  dyadmax  25924  itgfsum  26152  dvnadd  26254  cpnord  26260  dvnfre  26277  dvmptfsum  26300  ply1divex  26460  fta1g  26493  plyco  26565  dgrcolem1  26597  dgrco  26599  dvnply2  26613  plydivex  26623  aaliou3lem2  26675  dvntaylp  26703  taylthlem1  26705  cxpmul2  27022  jensen  27321  ftalem2  27406  bcmono  27609  bposlem5  27620  lgsquad2lem2  27717  dchrisumlem1  27821  dchrisum0flb  27842  pntpbnd1  27918  pntlemf  27937  qabvle  27957  qabvexp  27958  ostthlem2  27960  ostth2lem2  27966  nosupbnd1lem5  28074  noinfbnd1lem5  28089  precsexlem8  28605  precsexlem9  28606  om2noseqrdg  28695  n0addscl  28735  n0mulscl  28736  eucliddivs  28767  peano5uzs  28795  expscllem  28821  expadds  28826  expsne0  28827  expsgt0  28828  pw2cut  28851  pw2cut2  28853  plngrotlem2  29271  lfuhgr2  29732  rusgrnumwwlk  30572  eupth2lems  30844  eupth2  30845  ipasslem1  31438  mdslmd1lem1  32932  mdslmd1lem2  32933  iuninc  33202  ssrelf  33256  nn0min  33458  nexple  33470  gsumwun  33683  gsumvsca1  33833  gsumvsca2  33834  domnprodn0  33885  unitprodclb  33990  1arithufdlem3  34124  cmppcmp  34536  esumfzf  34747  sseqp1  35073  rrvsum  35132  signstfvc  35249  bnj1174  35679  subfacp1lem6  36036  mrsubvrs  36373  bccolsum  36596  iprodefisumlem  36597  faclimlem1  36600  onsuct0  37321  findfvcl  37332  poimirlem28  38659  sdclem2  38769  seqpo  38774  incsequz  38775  mettrifi  38784  heiborlem4  38841  bfplem1  38849  pclfinclN  41100  uzindd  43121  indstrd  43336  sn-sup2  43648  incssnn0  43815  mzpexpmpt  43849  pell14qrexpclnn0  43966  monotuz  44041  rmxypos  44047  jm2.17a  44060  jm2.17b  44061  rmygeid  44064  jm2.18  44088  jm2.19lem3  44091  jm2.15nn0  44103  jm2.16nn0  44104  dfac11  44157  pwslnm  44189  hbtlem5  44223  cnsrexpcl  44260  cantnfresb  44419  onmcl  44426  naddonnn  44490  relexpxpnnidm  44796  relexpiidm  44797  relexpss1d  44798  iunrelexpmin1  44801  relexpmulnn  44802  iunrelexpmin2  44805  relexp0a  44809  trclimalb2  44819  dvgrat  45389  relpfrlem  46036  trfr  46045  lmodvsmdi  49584  tfis2d  50955