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 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  39  imim2d  51  imim3i  58  loowoz  99  cbv1  1974  ralimdaa  2784  reuss2  3622  dfwe2  4763  tfindsg  4841  tfinds2  4844  tfinds3  4845  ordom  4855  findsg  4873  finds2  4874  ssrel  4965  ssrel2  4967  ssrelrel  4977  funfvima2  5975  isofrlem  6061  tfr3  6661  tz7.48lem  6699  oaordi  6790  oeordi  6831  nnaordi  6862  nnawordi  6865  nneneq  7291  ac6sfi  7352  domunfican  7380  fodomfi  7386  finsschain  7414  marypha1lem  7439  inf3lem2  7585  inf3lem5  7588  cantnfval2  7625  cantnflt  7628  cantnfp1lem3  7637  cnfcom  7658  dfac12lem3  8026  ackbij1lem16  8116  sornom  8158  infpssrlem4  8187  fin23lem34  8227  fin23lem36  8229  isf32lem1  8234  isf32lem2  8235  zorn2lem4  8380  zorn2lem5  8381  zorn2lem6  8382  zorn2lem7  8383  ttukeylem5  8394  pwfseqlem3  8536  wunfi  8597  grudomon  8693  prlem934  8911  sup2  9965  nnaddcl  10023  nnmulcl  10024  peano5uzi  10359  uzind2  10363  uzindOLD  10365  fzind  10369  zindd  10372  uzaddcl  10534  uzwo  10540  uzwoOLD  10541  om2uzlti  11291  seqcl2  11342  seqfveq2  11346  seqshft2  11350  monoord  11354  seqsplit  11357  seqcaopr3  11359  seqf1olem2a  11362  seqf1o  11365  seqid2  11370  seqhomo  11371  ser1const  11380  expcllem  11393  expeq0  11411  mulexp  11420  expadd  11423  expmul  11426  leexp2r  11438  leexp1a  11439  bernneq  11506  modexp  11515  facdiv  11579  facwordi  11581  faclbnd  11582  faclbnd4lem4  11588  faclbnd6  11591  hashgadd  11652  hashmap  11699  hashf1lem2  11706  hashf1  11707  seqcoll  11713  cjexp  11956  absexp  12110  rlimsqzlem  12443  lo1le  12446  iseraltlem2  12477  fsum2d  12556  fsumabs  12581  fsumrlim  12591  fsumo1  12592  fsumiun  12601  binom  12610  bcxmas  12616  climcndslem1  12630  climcndslem2  12631  cvgrat  12661  demoivreALT  12803  ruclem8  12837  ruclem9  12838  dvdsfac  12905  bitsinv1  12955  sadcadd  12971  sadadd2  12973  saddisjlem  12977  smuval2  12995  smupvallem  12996  smu01lem  12998  smupval  13001  smueqlem  13003  smumullem  13005  gcdmultiple  13051  rplpwr  13057  nn0seqcvgd  13062  seq1st  13063  alginv  13067  algcvga  13071  algfx  13072  prmdvdsexp  13115  prmfac1  13119  eulerthlem2  13172  pcmpt  13262  pcfac  13269  prmpwdvds  13273  prmreclem4  13288  vdwlem10  13359  ramcl  13398  mreexexd  13874  frmdgsum  14808  mulgnnass  14919  mhmmulg  14923  gsumwrev  15163  sylow1lem1  15233  efginvrel2  15360  efgsrel  15367  gsum2d  15547  ablfac1eulem  15631  pgpfac  15643  mplcoe1  16529  mplcoe3  16530  mplcoe2  16531  cnfldexp  16735  tgcl  17035  fiuncmp  17468  2ndcsep  17523  1stcelcls  17525  ptcmpfi  17846  tmdmulg  18123  tmdgsum  18126  imasdsf1olem  18404  fsumcn  18901  caubl  19261  caublcls  19262  ovolunlem1a  19393  ovolfiniun  19398  ovolicc2lem3  19416  volfiniun  19442  voliunlem1  19445  volsuplem  19450  volsup  19451  dyadmax  19491  itgfsum  19719  dvnadd  19816  dvnres  19818  cpnord  19822  dvnfre  19839  dvmptfsum  19860  ply1divex  20060  fta1g  20091  plyco  20161  dgrcolem1  20192  dgrco  20194  dvnply2  20205  plydivex  20215  aaliou3lem2  20261  dvntaylp  20288  taylthlem1  20290  cxpmul2  20581  jensen  20828  ftalem2  20857  bcmono  21062  bposlem5  21073  lgsquad2lem2  21144  dchrisumlem1  21184  dchrisum0flb  21205  pntpbnd1  21281  pntlemf  21300  qabvle  21320  qabvexp  21321  ostthlem2  21323  ostth2lem2  21329  eupath2  21703  gxnn0add  21863  gxnn0mul  21866  ipasslem1  22333  mdslmd1lem1  23829  mdslmd1lem2  23830  iuninc  24012  ofldchr  24245  esumfzf  24460  rrvsum  24713  subfacp1lem6  24872  cvmliftlem7  24979  cvmliftlem10  24982  clim2prod  25217  prodfn0  25223  prodfrec  25224  ntrivcvgfvn0  25228  fprodabs  25298  fprodefsum  25299  fprod2d  25306  iprodefisumlem  25318  binomfallfac  25358  faclimlem1  25363  trpredmintr  25510  wfr3g  25538  frr3g  25582  bpolycl  26099  onsuct0  26192  findfvcl  26203  sdclem2  26447  seqpo  26452  incsequz  26453  mettrifi  26464  heiborlem4  26524  bfplem1  26532  incssnn0  26766  mzpexpmpt  26803  pell14qrexpclnn0  26930  monotuz  27005  expmordi  27011  rmxypos  27013  jm2.17a  27026  jm2.17b  27027  rmygeid  27030  jm2.18  27060  jm2.19lem3  27063  jm2.15nn0  27075  jm2.16nn0  27076  dfac11  27138  pwslnm  27174  hbtlem5  27310  cnsrexpcl  27348  cshweqrep  28275  bnj1174  29373  pclfinclN  30748
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator