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

Theorem anim12d 547
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 22 . 2  |-  ( ph  ->  ( ( ch  /\  ta )  ->  ( ch 
/\  ta ) ) )
41, 2, 3syl2and 470 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anim1d  548  anim2d  549  prth  555  im2anan9  809  anim12dan  811  3anim123d  1261  2euswap  2330  ssunsn2  3918  disjiun  4162  soss  4481  wess  4529  ordtri3  4577  oneqmini  4592  ordom  4813  frinxp  4902  trin2  5216  xp11  5263  funss  5431  fun  5566  dff13  5963  f1eqcocnv  5987  isores3  6014  isosolem  6026  isowe2  6029  f1oweALT  6033  f1o2ndf1  6413  tposfn2  6460  tposf1o2  6464  smo11  6585  tfrlem1  6595  tz7.48lem  6657  om00  6777  omsmo  6856  ixpfi2  7363  elfiun  7393  supmo  7413  alephord  7912  cardaleph  7926  dfac5  7965  fin1a2lem9  8244  axdc3lem2  8287  zorn2lem6  8337  grudomon  8648  indpi  8740  genpnmax  8840  reclem3pr  8882  reclem4pr  8883  suplem1pr  8885  supsrlem  8942  lemul12b  9823  fimaxre  9911  lbreu  9914  supmullem2  9931  cju  9952  nnind  9974  uz11  10464  xrre2  10714  qbtwnre  10741  xrsupexmnf  10839  xrinfmexpnf  10840  ico0  10918  ioc0  10919  sqrlem6  12008  o1lo1  12286  ruclem9  12792  isprm3  13043  eulerthlem2  13126  prmdiveq  13130  ramub2  13337  lubun  14505  ipodrsima  14546  spwpr4  14618  dirtr  14636  mulgpropd  14878  dprdss  15542  subrgdvds  15837  epttop  17028  cnpresti  17306  cnprest  17307  lmmo  17398  1stcrest  17469  lly1stc  17512  txcnp  17605  addcnlem  18847  caussi  19203  bcthlem5  19234  ovollb2lem  19337  voliunlem1  19397  ioombl1lem4  19408  rolle  19827  c1lip1  19834  c1lip3  19836  ulmval  20249  sqf11  20875  fsumvma  20950  dchrelbas3  20975  constr3trllem2  21591  4cycl4v4e  21606  4cycl4dv  21607  eupai  21642  subgoablo  21852  nmcvcn  22144  sspmval  22185  sspival  22190  sspimsval  22192  sspph  22309  shsubcl  22676  shorth  22750  5oalem6  23114  strlem1  23706  atexch  23837  cdj3i  23897  xrofsup  24079  ishashinf  24112  cnre2csqima  24262  erdszelem9  24838  erdsze2lem2  24843  dedekind  25140  funpsstri  25335  dfon2lem4  25356  dfon2  25362  trpredrec  25455  frmin  25456  wfrlem4  25473  frrlem4  25498  nocvxminlem  25558  nocvxmin  25559  nofulllem5  25574  brbtwn2  25748  axeuclidlem  25805  axcontlem9  25815  axcontlem10  25816  btwnswapid  25855  ifscgr  25882  hilbert1.2  25993  supadd  26138  ltflcei  26140  mblfinlem2  26144  elicc3  26210  tailfb  26296  fzmul  26334  metf1o  26351  ismtycnv  26401  ismtyres  26407  crngohomfo  26506  prtlem50  26584  pm11.59  27458  infrglb  27589  afvres  27903  swrdnd  28001  swrdccat3  28029  usgra2wlkspthlem2  28037  usgra2adedgspthlem1  28043  usgra2adedgwlkon  28047  usg2wlkonot  28080  usg2wotspth  28081  2pthfrgrarn2  28114  frgranbnb  28124  lubunNEW  29456  hlhgt2  29871  hl2at  29887  2llnjN  30049  2lplnj  30102  linepsubN  30234  cdlemg33b0  31183  dvh3dim3N  31932  mapdh9a  32273
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 178  df-an 361
  Copyright terms: Public domain W3C validator