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  2633  reuss2  3461  dfwe2  4589  tfindsg  4667  tfinds2  4670  tfinds3  4671  ordom  4681  findsg  4699  finds2  4700  ssrel  4792  ssrelrel  4803  funfvima2  5770  isofrlem  5853  tfr3  6431  tz7.48lem  6469  oaordi  6560  oeordi  6601  nnaordi  6632  nnawordi  6635  nneneq  7060  ac6sfi  7117  domunfican  7145  fodomfi  7151  finsschain  7178  marypha1lem  7202  inf3lem2  7346  inf3lem5  7349  cantnfval2  7386  cantnflt  7389  cantnfp1lem3  7398  cnfcom  7419  dfac12lem3  7787  ackbij1lem16  7877  sornom  7919  infpssrlem4  7948  fin23lem34  7988  fin23lem36  7990  isf32lem1  7995  isf32lem2  7996  zorn2lem4  8142  zorn2lem5  8143  zorn2lem6  8144  zorn2lem7  8145  ttukeylem5  8156  pwfseqlem3  8298  wunfi  8359  grudomon  8455  prlem934  8673  sup2  9726  nnaddcl  9784  nnmulcl  9785  peano5uzi  10116  uzind2  10120  uzindOLD  10122  fzind  10126  zindd  10129  uzaddcl  10291  uzwo  10297  uzwoOLD  10298  om2uzlti  11029  seqcl2  11080  seqfveq2  11084  seqshft2  11088  monoord  11092  seqsplit  11095  seqcaopr3  11097  seqf1olem2a  11100  seqf1o  11103  seqid2  11108  seqhomo  11109  ser1const  11118  expcllem  11130  expeq0  11148  mulexp  11157  expadd  11160  expmul  11163  leexp2r  11175  leexp1a  11176  bernneq  11243  modexp  11252  facdiv  11316  facwordi  11318  faclbnd  11319  faclbnd4lem4  11325  faclbnd6  11328  hashgadd  11375  hashmap  11403  hashf1lem2  11410  hashf1  11411  seqcoll  11417  cjexp  11651  absexp  11805  rlimsqzlem  12138  lo1le  12141  iseraltlem2  12171  fsum2d  12250  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  binom  12304  bcxmas  12310  climcndslem1  12324  climcndslem2  12325  cvgrat  12355  demoivreALT  12497  ruclem8  12531  ruclem9  12532  dvdsfac  12599  bitsinv1  12649  sadcadd  12665  sadadd2  12667  saddisjlem  12671  smuval2  12689  smupvallem  12690  smu01lem  12692  smupval  12695  smueqlem  12697  smumullem  12699  gcdmultiple  12745  rplpwr  12751  nn0seqcvgd  12756  seq1st  12757  alginv  12761  algcvga  12765  algfx  12766  prmdvdsexp  12809  prmfac1  12813  eulerthlem2  12866  pcmpt  12956  pcfac  12963  prmpwdvds  12967  prmreclem4  12982  vdwlem10  13053  ramcl  13092  mreexexd  13566  frmdgsum  14500  mulgnnass  14611  mhmmulg  14615  gsumwrev  14855  sylow1lem1  14925  efginvrel2  15052  efgsrel  15059  gsum2d  15239  ablfac1eulem  15323  pgpfac  15335  mplcoe1  16225  mplcoe3  16226  mplcoe2  16227  cnfldexp  16423  tgcl  16723  fiuncmp  17147  2ndcsep  17201  1stcelcls  17203  ptcmpfi  17520  tmdmulg  17791  tmdgsum  17794  imasdsf1olem  17953  fsumcn  18390  caubl  18749  caublcls  18750  ovolunlem1a  18871  ovolfiniun  18876  ovolicc2lem3  18894  volfiniun  18920  voliunlem1  18923  volsuplem  18928  volsup  18929  dyadmax  18969  itgfsum  19197  dvnadd  19294  dvnres  19296  cpnord  19300  dvnfre  19317  dvmptfsum  19338  ply1divex  19538  fta1g  19569  plyco  19639  dgrcolem1  19670  dgrco  19672  dvnply2  19683  plydivex  19693  aaliou3lem2  19739  dvntaylp  19766  taylthlem1  19768  cxpmul2  20052  jensen  20299  ftalem2  20327  bcmono  20532  bposlem5  20543  lgsquad2lem2  20614  dchrisumlem1  20654  dchrisum0flb  20675  pntpbnd1  20751  pntlemf  20770  qabvle  20790  qabvexp  20791  ostthlem2  20793  ostth2lem2  20799  gxnn0add  20957  gxnn0mul  20960  ipasslem1  21425  mdslmd1lem1  22921  mdslmd1lem2  22922  iuninc  23174  subfacp1lem6  23731  cvmliftlem7  23837  cvmliftlem10  23840  eupath2  23919  faclim  24126  trpredmintr  24305  wfr3g  24326  frr3g  24351  bpolycl  24859  onsuct0  24952  findfvcl  24963  sdclem2  26555  seqpo  26560  incsequz  26561  mettrifi  26576  heiborlem4  26641  bfplem1  26649  incssnn0  26889  mzpexpmpt  26926  pell14qrexpclnn0  27054  monotuz  27129  expmordi  27135  rmxypos  27137  jm2.17a  27150  jm2.17b  27151  rmygeid  27154  jm2.18  27184  jm2.19lem3  27187  jm2.15nn0  27199  jm2.16nn0  27200  dfac11  27263  pwslnm  27299  hbtlem5  27435  cnsrexpcl  27473  bnj1174  29349  pclfinclN  30761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator