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  2728  reuss2  3566  dfwe2  4704  tfindsg  4782  tfinds2  4785  tfinds3  4786  ordom  4796  findsg  4814  finds2  4815  ssrel  4906  ssrel2  4908  ssrelrel  4918  funfvima2  5915  isofrlem  6001  tfr3  6598  tz7.48lem  6636  oaordi  6727  oeordi  6768  nnaordi  6799  nnawordi  6802  nneneq  7228  ac6sfi  7289  domunfican  7317  fodomfi  7323  finsschain  7350  marypha1lem  7375  inf3lem2  7519  inf3lem5  7522  cantnfval2  7559  cantnflt  7562  cantnfp1lem3  7571  cnfcom  7592  dfac12lem3  7960  ackbij1lem16  8050  sornom  8092  infpssrlem4  8121  fin23lem34  8161  fin23lem36  8163  isf32lem1  8168  isf32lem2  8169  zorn2lem4  8314  zorn2lem5  8315  zorn2lem6  8316  zorn2lem7  8317  ttukeylem5  8328  pwfseqlem3  8470  wunfi  8531  grudomon  8627  prlem934  8845  sup2  9898  nnaddcl  9956  nnmulcl  9957  peano5uzi  10292  uzind2  10296  uzindOLD  10298  fzind  10302  zindd  10305  uzaddcl  10467  uzwo  10473  uzwoOLD  10474  om2uzlti  11219  seqcl2  11270  seqfveq2  11274  seqshft2  11278  monoord  11282  seqsplit  11285  seqcaopr3  11287  seqf1olem2a  11290  seqf1o  11293  seqid2  11298  seqhomo  11299  ser1const  11308  expcllem  11321  expeq0  11339  mulexp  11348  expadd  11351  expmul  11354  leexp2r  11366  leexp1a  11367  bernneq  11434  modexp  11443  facdiv  11507  facwordi  11509  faclbnd  11510  faclbnd4lem4  11516  faclbnd6  11519  hashgadd  11580  hashmap  11627  hashf1lem2  11634  hashf1  11635  seqcoll  11641  cjexp  11884  absexp  12038  rlimsqzlem  12371  lo1le  12374  iseraltlem2  12405  fsum2d  12484  fsumabs  12509  fsumrlim  12519  fsumo1  12520  fsumiun  12529  binom  12538  bcxmas  12544  climcndslem1  12558  climcndslem2  12559  cvgrat  12589  demoivreALT  12731  ruclem8  12765  ruclem9  12766  dvdsfac  12833  bitsinv1  12883  sadcadd  12899  sadadd2  12901  saddisjlem  12905  smuval2  12923  smupvallem  12924  smu01lem  12926  smupval  12929  smueqlem  12931  smumullem  12933  gcdmultiple  12979  rplpwr  12985  nn0seqcvgd  12990  seq1st  12991  alginv  12995  algcvga  12999  algfx  13000  prmdvdsexp  13043  prmfac1  13047  eulerthlem2  13100  pcmpt  13190  pcfac  13197  prmpwdvds  13201  prmreclem4  13216  vdwlem10  13287  ramcl  13326  mreexexd  13802  frmdgsum  14736  mulgnnass  14847  mhmmulg  14851  gsumwrev  15091  sylow1lem1  15161  efginvrel2  15288  efgsrel  15295  gsum2d  15475  ablfac1eulem  15559  pgpfac  15571  mplcoe1  16457  mplcoe3  16458  mplcoe2  16459  cnfldexp  16659  tgcl  16959  fiuncmp  17391  2ndcsep  17445  1stcelcls  17447  ptcmpfi  17768  tmdmulg  18045  tmdgsum  18048  imasdsf1olem  18313  fsumcn  18773  caubl  19133  caublcls  19134  ovolunlem1a  19261  ovolfiniun  19266  ovolicc2lem3  19284  volfiniun  19310  voliunlem1  19313  volsuplem  19318  volsup  19319  dyadmax  19359  itgfsum  19587  dvnadd  19684  dvnres  19686  cpnord  19690  dvnfre  19707  dvmptfsum  19728  ply1divex  19928  fta1g  19959  plyco  20029  dgrcolem1  20060  dgrco  20062  dvnply2  20073  plydivex  20083  aaliou3lem2  20129  dvntaylp  20156  taylthlem1  20158  cxpmul2  20449  jensen  20696  ftalem2  20725  bcmono  20930  bposlem5  20941  lgsquad2lem2  21012  dchrisumlem1  21052  dchrisum0flb  21073  pntpbnd1  21149  pntlemf  21168  qabvle  21188  qabvexp  21189  ostthlem2  21191  ostth2lem2  21197  eupath2  21552  gxnn0add  21712  gxnn0mul  21715  ipasslem1  22182  mdslmd1lem1  23678  mdslmd1lem2  23679  iuninc  23857  ofldchr  24072  esumfzf  24257  rrvsum  24493  subfacp1lem6  24652  cvmliftlem7  24759  cvmliftlem10  24762  clim2prod  24997  prodfn0  25003  prodfrec  25004  ntrivcvgfvn0  25008  fprodabs  25078  fprodefsum  25079  faclimlem1  25122  trpredmintr  25260  wfr3g  25281  frr3g  25306  bpolycl  25814  onsuct0  25907  findfvcl  25918  sdclem2  26139  seqpo  26144  incsequz  26145  mettrifi  26156  heiborlem4  26216  bfplem1  26224  incssnn0  26458  mzpexpmpt  26495  pell14qrexpclnn0  26622  monotuz  26697  expmordi  26703  rmxypos  26705  jm2.17a  26718  jm2.17b  26719  rmygeid  26722  jm2.18  26752  jm2.19lem3  26755  jm2.15nn0  26767  jm2.16nn0  26768  dfac11  26831  pwslnm  26867  hbtlem5  27003  cnsrexpcl  27041  bnj1174  28712  pclfinclN  30066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator