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

Theorem a2d 23
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 15 1  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mpdd  36  imim2d  48  imim3i  55  loowoz  96  ralimdaa  2620  reuss2  3448  dfwe2  4573  tfindsg  4651  tfinds2  4654  tfinds3  4655  ordom  4665  findsg  4683  finds2  4684  ssrel  4776  ssrelrel  4787  funfvima2  5754  isofrlem  5837  tfr3  6415  tz7.48lem  6453  oaordi  6544  oeordi  6585  nnaordi  6616  nnawordi  6619  nneneq  7044  ac6sfi  7101  domunfican  7129  fodomfi  7135  finsschain  7162  marypha1lem  7186  inf3lem2  7330  inf3lem5  7333  cantnfval2  7370  cantnflt  7373  cantnfp1lem3  7382  cnfcom  7403  dfac12lem3  7771  ackbij1lem16  7861  sornom  7903  infpssrlem4  7932  fin23lem34  7972  fin23lem36  7974  isf32lem1  7979  isf32lem2  7980  zorn2lem4  8126  zorn2lem5  8127  zorn2lem6  8128  zorn2lem7  8129  ttukeylem5  8140  pwfseqlem3  8282  wunfi  8343  grudomon  8439  prlem934  8657  sup2  9710  nnaddcl  9768  nnmulcl  9769  peano5uzi  10100  uzind2  10104  uzindOLD  10106  fzind  10110  zindd  10113  uzaddcl  10275  uzwo  10281  uzwoOLD  10282  om2uzlti  11013  seqcl2  11064  seqfveq2  11068  seqshft2  11072  monoord  11076  seqsplit  11079  seqcaopr3  11081  seqf1olem2a  11084  seqf1o  11087  seqid2  11092  seqhomo  11093  ser1const  11102  expcllem  11114  expeq0  11132  mulexp  11141  expadd  11144  expmul  11147  leexp2r  11159  leexp1a  11160  bernneq  11227  modexp  11236  facdiv  11300  facwordi  11302  faclbnd  11303  faclbnd4lem4  11309  faclbnd6  11312  hashgadd  11359  hashmap  11387  hashf1lem2  11394  hashf1  11395  seqcoll  11401  cjexp  11635  absexp  11789  rlimsqzlem  12122  lo1le  12125  iseraltlem2  12155  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  binom  12288  bcxmas  12294  climcndslem1  12308  climcndslem2  12309  cvgrat  12339  demoivreALT  12481  ruclem8  12515  ruclem9  12516  dvdsfac  12583  bitsinv1  12633  sadcadd  12649  sadadd2  12651  saddisjlem  12655  smuval2  12673  smupvallem  12674  smu01lem  12676  smupval  12679  smueqlem  12681  smumullem  12683  gcdmultiple  12729  rplpwr  12735  nn0seqcvgd  12740  seq1st  12741  alginv  12745  algcvga  12749  algfx  12750  prmdvdsexp  12793  prmfac1  12797  eulerthlem2  12850  pcmpt  12940  pcfac  12947  prmpwdvds  12951  prmreclem4  12966  vdwlem10  13037  ramcl  13076  mreexexd  13550  frmdgsum  14484  mulgnnass  14595  mhmmulg  14599  gsumwrev  14839  sylow1lem1  14909  efginvrel2  15036  efgsrel  15043  gsum2d  15223  ablfac1eulem  15307  pgpfac  15319  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  cnfldexp  16407  tgcl  16707  fiuncmp  17131  2ndcsep  17185  1stcelcls  17187  ptcmpfi  17504  tmdmulg  17775  tmdgsum  17778  imasdsf1olem  17937  fsumcn  18374  caubl  18733  caublcls  18734  ovolunlem1a  18855  ovolfiniun  18860  ovolicc2lem3  18878  volfiniun  18904  voliunlem1  18907  volsuplem  18912  volsup  18913  dyadmax  18953  itgfsum  19181  dvnadd  19278  dvnres  19280  cpnord  19284  dvnfre  19301  dvmptfsum  19322  ply1divex  19522  fta1g  19553  plyco  19623  dgrcolem1  19654  dgrco  19656  dvnply2  19667  plydivex  19677  aaliou3lem2  19723  dvntaylp  19750  taylthlem1  19752  cxpmul2  20036  jensen  20283  ftalem2  20311  bcmono  20516  bposlem5  20527  lgsquad2lem2  20598  dchrisumlem1  20638  dchrisum0flb  20659  pntpbnd1  20735  pntlemf  20754  qabvle  20774  qabvexp  20775  ostthlem2  20777  ostth2lem2  20783  gxnn0add  20941  gxnn0mul  20944  ipasslem1  21409  mdslmd1lem1  22905  mdslmd1lem2  22906  iuninc  23158  subfacp1lem6  23716  cvmliftlem7  23822  cvmliftlem10  23825  eupath2  23904  trpredmintr  24234  wfr3g  24255  frr3g  24280  bpolycl  24787  onsuct0  24880  findfvcl  24891  sdclem2  26452  seqpo  26457  incsequz  26458  mettrifi  26473  heiborlem4  26538  bfplem1  26546  incssnn0  26786  mzpexpmpt  26823  pell14qrexpclnn0  26951  monotuz  27026  expmordi  27032  rmxypos  27034  jm2.17a  27047  jm2.17b  27048  rmygeid  27051  jm2.18  27081  jm2.19lem3  27084  jm2.15nn0  27096  jm2.16nn0  27097  dfac11  27160  pwslnm  27196  hbtlem5  27332  cnsrexpcl  27370  bnj1174  29033  pclfinclN  30139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator