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

Theorem a2d 24
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 6 . 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  38  imim2d  50  imim3i  57  loowoz  98  ralimdaa  2751  reuss2  3589  dfwe2  4729  tfindsg  4807  tfinds2  4810  tfinds3  4811  ordom  4821  findsg  4839  finds2  4840  ssrel  4931  ssrel2  4933  ssrelrel  4943  funfvima2  5941  isofrlem  6027  tfr3  6627  tz7.48lem  6665  oaordi  6756  oeordi  6797  nnaordi  6828  nnawordi  6831  nneneq  7257  ac6sfi  7318  domunfican  7346  fodomfi  7352  finsschain  7379  marypha1lem  7404  inf3lem2  7548  inf3lem5  7551  cantnfval2  7588  cantnflt  7591  cantnfp1lem3  7600  cnfcom  7621  dfac12lem3  7989  ackbij1lem16  8079  sornom  8121  infpssrlem4  8150  fin23lem34  8190  fin23lem36  8192  isf32lem1  8197  isf32lem2  8198  zorn2lem4  8343  zorn2lem5  8344  zorn2lem6  8345  zorn2lem7  8346  ttukeylem5  8357  pwfseqlem3  8499  wunfi  8560  grudomon  8656  prlem934  8874  sup2  9928  nnaddcl  9986  nnmulcl  9987  peano5uzi  10322  uzind2  10326  uzindOLD  10328  fzind  10332  zindd  10335  uzaddcl  10497  uzwo  10503  uzwoOLD  10504  om2uzlti  11253  seqcl2  11304  seqfveq2  11308  seqshft2  11312  monoord  11316  seqsplit  11319  seqcaopr3  11321  seqf1olem2a  11324  seqf1o  11327  seqid2  11332  seqhomo  11333  ser1const  11342  expcllem  11355  expeq0  11373  mulexp  11382  expadd  11385  expmul  11388  leexp2r  11400  leexp1a  11401  bernneq  11468  modexp  11477  facdiv  11541  facwordi  11543  faclbnd  11544  faclbnd4lem4  11550  faclbnd6  11553  hashgadd  11614  hashmap  11661  hashf1lem2  11668  hashf1  11669  seqcoll  11675  cjexp  11918  absexp  12072  rlimsqzlem  12405  lo1le  12408  iseraltlem2  12439  fsum2d  12518  fsumabs  12543  fsumrlim  12553  fsumo1  12554  fsumiun  12563  binom  12572  bcxmas  12578  climcndslem1  12592  climcndslem2  12593  cvgrat  12623  demoivreALT  12765  ruclem8  12799  ruclem9  12800  dvdsfac  12867  bitsinv1  12917  sadcadd  12933  sadadd2  12935  saddisjlem  12939  smuval2  12957  smupvallem  12958  smu01lem  12960  smupval  12963  smueqlem  12965  smumullem  12967  gcdmultiple  13013  rplpwr  13019  nn0seqcvgd  13024  seq1st  13025  alginv  13029  algcvga  13033  algfx  13034  prmdvdsexp  13077  prmfac1  13081  eulerthlem2  13134  pcmpt  13224  pcfac  13231  prmpwdvds  13235  prmreclem4  13250  vdwlem10  13321  ramcl  13360  mreexexd  13836  frmdgsum  14770  mulgnnass  14881  mhmmulg  14885  gsumwrev  15125  sylow1lem1  15195  efginvrel2  15322  efgsrel  15329  gsum2d  15509  ablfac1eulem  15593  pgpfac  15605  mplcoe1  16491  mplcoe3  16492  mplcoe2  16493  cnfldexp  16697  tgcl  16997  fiuncmp  17429  2ndcsep  17483  1stcelcls  17485  ptcmpfi  17806  tmdmulg  18083  tmdgsum  18086  imasdsf1olem  18364  fsumcn  18861  caubl  19221  caublcls  19222  ovolunlem1a  19353  ovolfiniun  19358  ovolicc2lem3  19376  volfiniun  19402  voliunlem1  19405  volsuplem  19410  volsup  19411  dyadmax  19451  itgfsum  19679  dvnadd  19776  dvnres  19778  cpnord  19782  dvnfre  19799  dvmptfsum  19820  ply1divex  20020  fta1g  20051  plyco  20121  dgrcolem1  20152  dgrco  20154  dvnply2  20165  plydivex  20175  aaliou3lem2  20221  dvntaylp  20248  taylthlem1  20250  cxpmul2  20541  jensen  20788  ftalem2  20817  bcmono  21022  bposlem5  21033  lgsquad2lem2  21104  dchrisumlem1  21144  dchrisum0flb  21165  pntpbnd1  21241  pntlemf  21260  qabvle  21280  qabvexp  21281  ostthlem2  21283  ostth2lem2  21289  eupath2  21663  gxnn0add  21823  gxnn0mul  21826  ipasslem1  22293  mdslmd1lem1  23789  mdslmd1lem2  23790  iuninc  23972  ofldchr  24205  esumfzf  24420  rrvsum  24673  subfacp1lem6  24832  cvmliftlem7  24939  cvmliftlem10  24942  clim2prod  25177  prodfn0  25183  prodfrec  25184  ntrivcvgfvn0  25188  fprodabs  25258  fprodefsum  25259  fprod2d  25266  iprodefisumlem  25278  binomfallfac  25316  faclimlem1  25318  trpredmintr  25456  wfr3g  25477  frr3g  25502  bpolycl  26010  onsuct0  26103  findfvcl  26114  sdclem2  26344  seqpo  26349  incsequz  26350  mettrifi  26361  heiborlem4  26421  bfplem1  26429  incssnn0  26663  mzpexpmpt  26700  pell14qrexpclnn0  26827  monotuz  26902  expmordi  26908  rmxypos  26910  jm2.17a  26923  jm2.17b  26924  rmygeid  26927  jm2.18  26957  jm2.19lem3  26960  jm2.15nn0  26972  jm2.16nn0  26973  dfac11  27036  pwslnm  27072  hbtlem5  27208  cnsrexpcl  27246  bnj1174  29090  pclfinclN  30444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator