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

Theorem anim12d 546
Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
Hypotheses
Ref Expression
anim12d.1  |-  ( ph  ->  ( ps  ->  ch ) )
anim12d.2  |-  ( ph  ->  ( th  ->  ta ) )
Assertion
Ref Expression
anim12d  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )

Proof of Theorem anim12d
StepHypRef Expression
1 anim12d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 anim12d.2 . 2  |-  ( ph  ->  ( th  ->  ta ) )
3 idd 21 . 2  |-  ( ph  ->  ( ( ch  /\  ta )  ->  ( ch 
/\  ta ) ) )
41, 2, 3syl2and 469 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anim1d  547  anim2d  548  prth  554  im2anan9  808  anim12dan  810  3anim123d  1259  2euswap  2232  ssunsn2  3789  disjiun  4029  soss  4348  wess  4396  ordtri3  4444  oneqmini  4459  ordom  4681  frinxp  4771  trin2  5082  xp11  5127  funss  5289  fun  5421  dff13  5799  f1eqcocnv  5821  isores3  5848  isosolem  5860  isowe2  5863  f1oweALT  5867  tposfn2  6272  tposf1o2  6276  smo11  6397  tfrlem1  6407  tz7.48lem  6469  om00  6589  omsmo  6668  ixpfi2  7170  elfiun  7199  supmo  7219  alephord  7718  cardaleph  7732  dfac5  7771  fin1a2lem9  8050  axdc3lem2  8093  zorn2lem6  8144  grudomon  8455  indpi  8547  genpnmax  8647  reclem3pr  8689  reclem4pr  8690  suplem1pr  8692  supsrlem  8749  lemul12b  9629  fimaxre  9717  lbreu  9720  supmullem2  9737  cju  9758  nnind  9780  uz11  10266  xrre2  10515  qbtwnre  10542  xrsupexmnf  10639  xrinfmexpnf  10640  ico0  10718  ioc0  10719  sqrlem6  11749  o1lo1  12027  ruclem9  12532  isprm3  12783  eulerthlem2  12866  prmdiveq  12870  ramub2  13077  lubun  14243  ipodrsima  14284  spwpr4  14356  dirtr  14374  mulgpropd  14616  dprdss  15280  subrgdvds  15575  epttop  16762  cnpresti  17032  cnprest  17033  lmmo  17124  1stcrest  17195  lly1stc  17238  txcnp  17330  addcnlem  18384  caussi  18739  bcthlem5  18766  ovollb2lem  18863  voliunlem1  18923  ioombl1lem4  18934  rolle  19353  c1lip1  19360  c1lip3  19362  ulmval  19775  sqf11  20393  fsumvma  20468  dchrelbas3  20493  subgoablo  20994  nmcvcn  21284  sspmval  21325  sspival  21330  sspimsval  21332  sspph  21449  shsubcl  21816  shorth  21890  5oalem6  22254  strlem1  22846  atexch  22977  cdj3i  23037  xrofsup  23270  cnre2csqima  23310  ishashinf  23404  erdszelem9  23745  erdsze2lem2  23750  eupai  23898  dedekind  24097  funpsstri  24192  dfon2lem4  24213  dfon2  24219  trpredrec  24312  frmin  24313  wfrlem4  24330  frrlem4  24355  nocvxminlem  24415  nocvxmin  24416  nofulllem5  24431  brbtwn2  24605  axeuclidlem  24662  axcontlem9  24672  axcontlem10  24673  btwnswapid  24712  ifscgr  24739  hilbert1.2  24850  supadd  24996  ltflcei  24998  oooeqim2  25156  intcont  25646  trnij  25718  icccon2  25803  icccon4  25805  ismonc  25917  iepiclem  25926  isepic  25927  propsrc  25971  elicc3  26331  tailfb  26429  fzmul  26546  metf1o  26572  ismtycnv  26629  ismtyres  26635  crngohomfo  26734  prtlem50  26814  pm11.59  27693  rfcnnnub  27810  infrglb  27825  afvres  28140  constr3trllem2  28397  4cycl4v4e  28412  4cycl4dv  28413  2pthfrgrarn2  28434  lubunNEW  29785  hlhgt2  30200  hl2at  30216  2llnjN  30378  2lplnj  30431  linepsubN  30563  cdlemg33b0  31512  dvh3dim3N  32261  mapdh9a  32602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator