MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a2d Structured version   Unicode version

Theorem a2d 25
Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)
Hypothesis
Ref Expression
a2d.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
a2d  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )

Proof of Theorem a2d
StepHypRef Expression
1 a2d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
2 ax-2 7 . 2  |-  ( ( ps  ->  ( ch  ->  th ) )  -> 
( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
31, 2syl 16 1  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mpdd  39  imim2d  51  imim3i  58  loowoz  99  cbv1  1977  ralimdaa  2790  reuss2  3609  dfwe2  4797  tfindsg  4875  tfinds2  4878  tfinds3  4879  ordom  4889  findsg  4907  finds2  4908  ssrel  4999  ssrel2  5001  ssrelrel  5011  funfvima2  6010  isofrlem  6096  tfr3  6696  tz7.48lem  6734  oaordi  6825  oeordi  6866  nnaordi  6897  nnawordi  6900  nneneq  7326  ac6sfi  7387  domunfican  7415  fodomfi  7421  finsschain  7449  marypha1lem  7474  inf3lem2  7620  inf3lem5  7623  cantnfval2  7660  cantnflt  7663  cantnfp1lem3  7672  cnfcom  7693  dfac12lem3  8063  ackbij1lem16  8153  sornom  8195  infpssrlem4  8224  fin23lem34  8264  fin23lem36  8266  isf32lem1  8271  isf32lem2  8272  zorn2lem4  8417  zorn2lem5  8418  zorn2lem6  8419  zorn2lem7  8420  ttukeylem5  8431  pwfseqlem3  8573  wunfi  8634  grudomon  8730  prlem934  8948  sup2  10002  nnaddcl  10060  nnmulcl  10061  peano5uzi  10396  uzind2  10400  uzindOLD  10402  fzind  10406  zindd  10409  uzaddcl  10571  uzwo  10577  uzwoOLD  10578  om2uzlti  11328  seqcl2  11379  seqfveq2  11383  seqshft2  11387  monoord  11391  seqsplit  11394  seqcaopr3  11396  seqf1olem2a  11399  seqf1o  11402  seqid2  11407  seqhomo  11408  ser1const  11417  expcllem  11430  expeq0  11448  mulexp  11457  expadd  11460  expmul  11463  leexp2r  11475  leexp1a  11476  bernneq  11543  modexp  11552  facdiv  11616  facwordi  11618  faclbnd  11619  faclbnd4lem4  11625  faclbnd6  11628  hashgadd  11689  hashmap  11736  hashf1lem2  11743  hashf1  11744  seqcoll  11750  cjexp  11993  absexp  12147  rlimsqzlem  12480  lo1le  12483  iseraltlem2  12514  fsum2d  12593  fsumabs  12618  fsumrlim  12628  fsumo1  12629  fsumiun  12638  binom  12647  bcxmas  12653  climcndslem1  12667  climcndslem2  12668  cvgrat  12698  demoivreALT  12840  ruclem8  12874  ruclem9  12875  dvdsfac  12942  bitsinv1  12992  sadcadd  13008  sadadd2  13010  saddisjlem  13014  smuval2  13032  smupvallem  13033  smu01lem  13035  smupval  13038  smueqlem  13040  smumullem  13042  gcdmultiple  13088  rplpwr  13094  nn0seqcvgd  13099  seq1st  13100  alginv  13104  algcvga  13108  algfx  13109  prmdvdsexp  13152  prmfac1  13156  eulerthlem2  13209  pcmpt  13299  pcfac  13306  prmpwdvds  13310  prmreclem4  13325  vdwlem10  13396  ramcl  13435  mreexexd  13911  frmdgsum  14845  mulgnnass  14956  mhmmulg  14960  gsumwrev  15200  sylow1lem1  15270  efginvrel2  15397  efgsrel  15404  gsum2d  15584  ablfac1eulem  15668  pgpfac  15680  mplcoe1  16566  mplcoe3  16567  mplcoe2  16568  cnfldexp  16772  tgcl  17072  fiuncmp  17505  2ndcsep  17560  1stcelcls  17562  ptcmpfi  17883  tmdmulg  18160  tmdgsum  18163  imasdsf1olem  18441  fsumcn  18938  caubl  19298  caublcls  19299  ovolunlem1a  19430  ovolfiniun  19435  ovolicc2lem3  19453  volfiniun  19479  voliunlem1  19482  volsuplem  19487  volsup  19488  dyadmax  19528  itgfsum  19754  dvnadd  19853  dvnres  19855  cpnord  19859  dvnfre  19876  dvmptfsum  19897  ply1divex  20097  fta1g  20128  plyco  20198  dgrcolem1  20229  dgrco  20231  dvnply2  20242  plydivex  20252  aaliou3lem2  20298  dvntaylp  20325  taylthlem1  20327  cxpmul2  20618  jensen  20865  ftalem2  20894  bcmono  21099  bposlem5  21110  lgsquad2lem2  21181  dchrisumlem1  21221  dchrisum0flb  21242  pntpbnd1  21318  pntlemf  21337  qabvle  21357  qabvexp  21358  ostthlem2  21360  ostth2lem2  21366  eupath2  21740  gxnn0add  21900  gxnn0mul  21903  ipasslem1  22370  mdslmd1lem1  23866  mdslmd1lem2  23867  iuninc  24046  ofldchr  24279  esumfzf  24494  rrvsum  24747  subfacp1lem6  24906  cvmliftlem7  25013  cvmliftlem10  25016  clim2prod  25251  prodfn0  25257  prodfrec  25258  ntrivcvgfvn0  25262  fprodabs  25332  fprodefsum  25333  fprod2d  25340  iprodefisumlem  25352  binomfallfac  25392  faclimlem1  25397  trpredmintr  25544  wfr3g  25572  frr3g  25616  bpolycl  26133  onsuct0  26226  findfvcl  26237  sdclem2  26488  seqpo  26493  incsequz  26494  mettrifi  26505  heiborlem4  26565  bfplem1  26573  incssnn0  26877  mzpexpmpt  26914  pell14qrexpclnn0  27041  monotuz  27116  expmordi  27122  rmxypos  27124  jm2.17a  27137  jm2.17b  27138  rmygeid  27141  jm2.18  27171  jm2.19lem3  27174  jm2.15nn0  27186  jm2.16nn0  27187  dfac11  27249  pwslnm  27285  hbtlem5  27421  cnsrexpcl  27459  cshweqrep  28406  bnj1174  29546  pclfinclN  30921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator