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  1629  cbv1v  2337  cbv1  2401  ralimdva  3090  reuss2  4216  ssrel  5639  ssrel2  5641  ssrelrel  5651  funfvima2  7025  isofrlem  7127  dfwe2  7537  tfindsg  7617  tfinds2  7620  tfinds3  7621  trom  7631  findsg  7655  finds2  7656  fpr3g  8004  wfr3g  8031  tfrlem1  8090  tfr3  8113  tz7.48lem  8155  oaordi  8252  oeordi  8293  nnaordi  8324  nnawordi  8327  nneneq  8807  ac6sfi  8893  domunfican  8922  fodomfi  8927  finsschain  8961  marypha1lem  9027  inf3lem2  9222  inf3lem5  9225  cantnfval2  9262  cantnflt  9265  cantnfp1lem3  9273  cnfcom  9293  trpredmintr  9314  dfac12lem3  9724  ackbij1lem16  9814  sornom  9856  infpssrlem4  9885  fin23lem34  9925  fin23lem36  9927  isf32lem1  9932  isf32lem2  9933  zorn2lem4  10078  zorn2lem5  10079  zorn2lem6  10080  zorn2lem7  10081  ttukeylem5  10092  pwfseqlem3  10239  wunfi  10300  grudomon  10396  prlem934  10612  sup2  11753  nnindd  11815  nnaddcl  11818  nnmulcl  11819  nnne0  11829  peano5uzi  12231  uzind2  12235  nn0indd  12239  fzind  12240  zindd  12243  uzaddcl  12465  uzwo  12472  om2uzlti  13488  seqcaopr3  13576  seqf1olem2a  13579  seqf1o  13582  ser1const  13597  expcllem  13611  expeq0  13630  mulexp  13639  expadd  13642  expmul  13645  expmordi  13702  leexp2r  13709  leexp1a  13710  bernneq  13761  modexp  13770  facdiv  13818  facwordi  13820  faclbnd  13821  faclbnd4lem4  13827  hashgadd  13909  hashmap  13967  hashf1lem2  13987  hashf1  13988  seqcoll  13995  cshweqrep  14351  relexpsucnnl  14558  relexpcnv  14563  relexpnndm  14569  relexpaddnn  14579  rlimsqzlem  15177  lo1le  15180  iseraltlem2  15211  fsum2d  15298  modfsummod  15321  fsumabs  15328  fsumrlim  15338  fsumo1  15339  fsumiun  15348  binom  15357  climcndslem1  15376  climcndslem2  15377  cvgrat  15410  clim2prod  15415  prodfn0  15421  prodfrec  15422  ntrivcvgfvn0  15426  fprodabs  15499  fprod2d  15506  binomfallfac  15566  bpolycl  15577  fprodefsum  15619  demoivreALT  15725  ruclem8  15761  ruclem9  15762  dvdsfac  15850  bitsinv1  15964  sadcadd  15980  sadadd2  15982  saddisjlem  15986  smuval2  16004  smupvallem  16005  smu01lem  16007  smupval  16010  smueqlem  16012  smumullem  16014  gcdmultipleOLD  16075  rplpwr  16082  nn0seqcvgd  16090  seq1st  16091  alginv  16095  algcvga  16099  algfx  16100  prmdvdsexp  16235  prmfac1  16241  eulerthlem2  16298  pcmpt  16408  pcfac  16415  prmpwdvds  16420  prmreclem4  16435  vdwlem10  16506  ramcl  16545  mreexexd  17105  frmdgsum  18243  mulgnnass  18480  mhmmulg  18486  gsumwrev  18712  gsmsymgrfix  18774  gsmsymgreq  18778  efginvrel2  19071  efgsrel  19078  gsum2dlem2  19310  ablfac1eulem  19413  pgpfac  19425  srgmulgass  19500  srgpcomp  19501  srgbinom  19514  lmodvsmmulgdi  19888  cnfldexp  20350  assamulgscm  20815  mplcoe1  20948  mplcoe3  20949  mplcoe5  20951  mptcoe1fsupp  21090  coe1fzgsumdlem  21176  coe1fzgsumd  21177  gsummoncoe1  21179  evl1gsumdlem  21226  evl1gsumd  21227  mdetunilem9  21471  mptcoe1matfsupp  21653  mp2pm2mplem4  21660  chpdmat  21692  tgcl  21820  fiuncmp  22255  2ndcsep  22310  1stcelcls  22312  ptcmpfi  22664  tmdgsum  22946  fsumcn  23721  caubl  24159  caublcls  24160  ovolunlem1a  24347  ovolfiniun  24352  volfiniun  24398  voliunlem1  24401  volsuplem  24406  volsup  24407  dyadmax  24449  itgfsum  24678  dvnadd  24780  cpnord  24786  dvnfre  24803  dvmptfsum  24826  ply1divex  24988  fta1g  25019  plyco  25089  dgrcolem1  25121  dgrco  25123  dvnply2  25134  plydivex  25144  aaliou3lem2  25190  dvntaylp  25217  taylthlem1  25219  cxpmul2  25531  jensen  25825  ftalem2  25910  bcmono  26112  bposlem5  26123  lgsquad2lem2  26220  dchrisumlem1  26324  dchrisum0flb  26345  pntpbnd1  26421  pntlemf  26440  qabvle  26460  qabvexp  26461  ostthlem2  26463  ostth2lem2  26469  rusgrnumwwlk  28013  eupth2lems  28275  eupth2  28276  ipasslem1  28866  mdslmd1lem1  30360  mdslmd1lem2  30361  iuninc  30573  ssrelf  30628  nn0min  30808  gsumle  31023  gsumvsca1  31152  gsumvsca2  31153  ofldchr  31186  cmppcmp  31476  nexple  31643  esumfzf  31703  sseqp1  32028  rrvsum  32087  signstfvc  32219  bnj1174  32650  lfuhgr2  32747  subfacp1lem6  32814  mrsubvrs  33151  bccolsum  33374  iprodefisumlem  33375  faclimlem1  33378  frr3g  33504  naddssim  33523  nosupbnd1lem5  33601  noinfbnd1lem5  33616  onsuct0  34316  findfvcl  34327  poimirlem28  35491  sdclem2  35586  seqpo  35591  incsequz  35592  mettrifi  35601  heiborlem4  35658  bfplem1  35666  pclfinclN  37650  fzindd  39667  uzindd  39668  nnaddcom  39946  nnadddir  39948  nnmulcom  39950  sn-sup2  40088  incssnn0  40177  mzpexpmpt  40211  pell14qrexpclnn0  40332  monotuz  40407  rmxypos  40413  jm2.17a  40426  jm2.17b  40427  rmygeid  40430  jm2.18  40454  jm2.19lem3  40457  jm2.15nn0  40469  jm2.16nn0  40470  dfac11  40531  pwslnm  40563  hbtlem5  40597  cnsrexpcl  40634  relexpxpnnidm  40929  relexpiidm  40930  relexpss1d  40931  iunrelexpmin1  40934  relexpmulnn  40935  iunrelexpmin2  40938  relexp0a  40942  trclimalb2  40952  dvgrat  41544  lmodvsmdi  45334  tfis2d  46000