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  2219  ssunsn2  3773  disjiun  4013  soss  4332  wess  4380  ordtri3  4428  oneqmini  4443  ordom  4665  frinxp  4755  trin2  5066  xp11  5111  funss  5273  fun  5405  dff13  5783  f1eqcocnv  5805  isores3  5832  isosolem  5844  isowe2  5847  f1oweALT  5851  tposfn2  6256  tposf1o2  6260  smo11  6381  tfrlem1  6391  tz7.48lem  6453  om00  6573  omsmo  6652  ixpfi2  7154  elfiun  7183  supmo  7203  alephord  7702  cardaleph  7716  dfac5  7755  fin1a2lem9  8034  axdc3lem2  8077  zorn2lem6  8128  grudomon  8439  indpi  8531  genpnmax  8631  reclem3pr  8673  reclem4pr  8674  suplem1pr  8676  supsrlem  8733  lemul12b  9613  fimaxre  9701  lbreu  9704  supmullem2  9721  cju  9742  nnind  9764  uz11  10250  xrre2  10499  qbtwnre  10526  xrsupexmnf  10623  xrinfmexpnf  10624  ico0  10702  ioc0  10703  sqrlem6  11733  o1lo1  12011  ruclem9  12516  isprm3  12767  eulerthlem2  12850  prmdiveq  12854  ramub2  13061  lubun  14227  ipodrsima  14268  spwpr4  14340  dirtr  14358  mulgpropd  14600  dprdss  15264  subrgdvds  15559  epttop  16746  cnpresti  17016  cnprest  17017  lmmo  17108  1stcrest  17179  lly1stc  17222  txcnp  17314  addcnlem  18368  caussi  18723  bcthlem5  18750  ovollb2lem  18847  voliunlem1  18907  ioombl1lem4  18918  rolle  19337  c1lip1  19344  c1lip3  19346  ulmval  19759  sqf11  20377  fsumvma  20452  dchrelbas3  20477  subgoablo  20978  nmcvcn  21268  sspmval  21309  sspival  21314  sspimsval  21316  sspph  21433  shsubcl  21800  shorth  21874  5oalem6  22238  strlem1  22830  atexch  22961  cdj3i  23021  xrofsup  23255  cnre2csqima  23295  ishashinf  23389  erdszelem9  23730  erdsze2lem2  23735  eupai  23883  dedekind  24082  funpsstri  24121  dfon2lem4  24142  dfon2  24148  trpredrec  24241  frmin  24242  wfrlem4  24259  frrlem4  24284  nocvxminlem  24344  nocvxmin  24345  nofulllem5  24360  brbtwn2  24533  axeuclidlem  24590  axcontlem9  24600  axcontlem10  24601  btwnswapid  24640  ifscgr  24667  hilbert1.2  24778  oooeqim2  25053  intcont  25543  trnij  25615  icccon2  25700  icccon4  25702  ismonc  25814  iepiclem  25823  isepic  25824  propsrc  25868  elicc3  26228  tailfb  26326  fzmul  26443  metf1o  26469  ismtycnv  26526  ismtyres  26532  crngohomfo  26631  prtlem50  26711  pm11.59  27590  rfcnnnub  27707  infrglb  27722  afvres  28034  lubunNEW  29163  hlhgt2  29578  hl2at  29594  2llnjN  29756  2lplnj  29809  linepsubN  29941  cdlemg33b0  30890  dvh3dim3N  31639  mapdh9a  31980
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