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  2743  reuss2  3581  dfwe2  4721  tfindsg  4799  tfinds2  4802  tfinds3  4803  ordom  4813  findsg  4831  finds2  4832  ssrel  4923  ssrel2  4925  ssrelrel  4935  funfvima2  5933  isofrlem  6019  tfr3  6619  tz7.48lem  6657  oaordi  6748  oeordi  6789  nnaordi  6820  nnawordi  6823  nneneq  7249  ac6sfi  7310  domunfican  7338  fodomfi  7344  finsschain  7371  marypha1lem  7396  inf3lem2  7540  inf3lem5  7543  cantnfval2  7580  cantnflt  7583  cantnfp1lem3  7592  cnfcom  7613  dfac12lem3  7981  ackbij1lem16  8071  sornom  8113  infpssrlem4  8142  fin23lem34  8182  fin23lem36  8184  isf32lem1  8189  isf32lem2  8190  zorn2lem4  8335  zorn2lem5  8336  zorn2lem6  8337  zorn2lem7  8338  ttukeylem5  8349  pwfseqlem3  8491  wunfi  8552  grudomon  8648  prlem934  8866  sup2  9920  nnaddcl  9978  nnmulcl  9979  peano5uzi  10314  uzind2  10318  uzindOLD  10320  fzind  10324  zindd  10327  uzaddcl  10489  uzwo  10495  uzwoOLD  10496  om2uzlti  11245  seqcl2  11296  seqfveq2  11300  seqshft2  11304  monoord  11308  seqsplit  11311  seqcaopr3  11313  seqf1olem2a  11316  seqf1o  11319  seqid2  11324  seqhomo  11325  ser1const  11334  expcllem  11347  expeq0  11365  mulexp  11374  expadd  11377  expmul  11380  leexp2r  11392  leexp1a  11393  bernneq  11460  modexp  11469  facdiv  11533  facwordi  11535  faclbnd  11536  faclbnd4lem4  11542  faclbnd6  11545  hashgadd  11606  hashmap  11653  hashf1lem2  11660  hashf1  11661  seqcoll  11667  cjexp  11910  absexp  12064  rlimsqzlem  12397  lo1le  12400  iseraltlem2  12431  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  binom  12564  bcxmas  12570  climcndslem1  12584  climcndslem2  12585  cvgrat  12615  demoivreALT  12757  ruclem8  12791  ruclem9  12792  dvdsfac  12859  bitsinv1  12909  sadcadd  12925  sadadd2  12927  saddisjlem  12931  smuval2  12949  smupvallem  12950  smu01lem  12952  smupval  12955  smueqlem  12957  smumullem  12959  gcdmultiple  13005  rplpwr  13011  nn0seqcvgd  13016  seq1st  13017  alginv  13021  algcvga  13025  algfx  13026  prmdvdsexp  13069  prmfac1  13073  eulerthlem2  13126  pcmpt  13216  pcfac  13223  prmpwdvds  13227  prmreclem4  13242  vdwlem10  13313  ramcl  13352  mreexexd  13828  frmdgsum  14762  mulgnnass  14873  mhmmulg  14877  gsumwrev  15117  sylow1lem1  15187  efginvrel2  15314  efgsrel  15321  gsum2d  15501  ablfac1eulem  15585  pgpfac  15597  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  cnfldexp  16689  tgcl  16989  fiuncmp  17421  2ndcsep  17475  1stcelcls  17477  ptcmpfi  17798  tmdmulg  18075  tmdgsum  18078  imasdsf1olem  18356  fsumcn  18853  caubl  19213  caublcls  19214  ovolunlem1a  19345  ovolfiniun  19350  ovolicc2lem3  19368  volfiniun  19394  voliunlem1  19397  volsuplem  19402  volsup  19403  dyadmax  19443  itgfsum  19671  dvnadd  19768  dvnres  19770  cpnord  19774  dvnfre  19791  dvmptfsum  19812  ply1divex  20012  fta1g  20043  plyco  20113  dgrcolem1  20144  dgrco  20146  dvnply2  20157  plydivex  20167  aaliou3lem2  20213  dvntaylp  20240  taylthlem1  20242  cxpmul2  20533  jensen  20780  ftalem2  20809  bcmono  21014  bposlem5  21025  lgsquad2lem2  21096  dchrisumlem1  21136  dchrisum0flb  21157  pntpbnd1  21233  pntlemf  21252  qabvle  21272  qabvexp  21273  ostthlem2  21275  ostth2lem2  21281  eupath2  21655  gxnn0add  21815  gxnn0mul  21818  ipasslem1  22285  mdslmd1lem1  23781  mdslmd1lem2  23782  iuninc  23964  ofldchr  24197  esumfzf  24412  rrvsum  24665  subfacp1lem6  24824  cvmliftlem7  24931  cvmliftlem10  24934  clim2prod  25169  prodfn0  25175  prodfrec  25176  ntrivcvgfvn0  25180  fprodabs  25250  fprodefsum  25251  fprod2d  25258  iprodefisumlem  25270  binomfallfac  25308  faclimlem1  25310  trpredmintr  25448  wfr3g  25469  frr3g  25494  bpolycl  26002  onsuct0  26095  findfvcl  26106  sdclem2  26336  seqpo  26341  incsequz  26342  mettrifi  26353  heiborlem4  26413  bfplem1  26421  incssnn0  26655  mzpexpmpt  26692  pell14qrexpclnn0  26819  monotuz  26894  expmordi  26900  rmxypos  26902  jm2.17a  26915  jm2.17b  26916  rmygeid  26919  jm2.18  26949  jm2.19lem3  26952  jm2.15nn0  26964  jm2.16nn0  26965  dfac11  27028  pwslnm  27064  hbtlem5  27200  cnsrexpcl  27238  bnj1174  29078  pclfinclN  30432
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator