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

Theorem anim12d 561
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 24 . 2  |-  ( ph  ->  ( ( ch  /\  ta )  ->  ( ch 
/\  ta ) ) )
41, 2, 3syl2and 481 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  anim1d  562  anim2d  563  prth  569  im2anan9  833  anim12dan  835  3anim123d  1304  mo3  2268  2euswap  2311  2moOLD  2315  ssunsn2  4116  disjiun  4371  soss  4745  wess  4793  ordtri3  4841  oneqmini  4856  frinxp  4992  trin2  5316  xp11  5365  funss  5527  fun  5669  fvcofneq  5954  dff13  6083  f1eqcocnv  6123  isores3  6150  isosolem  6162  isowe2  6165  ordom  6626  f1oweALT  6701  f1o2ndf1  6825  tposfn2  6913  tposf1o2  6917  smo11  6971  tz7.48lem  7042  om00  7160  omsmo  7239  ixpfi2  7751  elfiun  7823  supmo  7844  alephord  8387  cardaleph  8401  dfac5  8440  fin1a2lem9  8719  axdc3lem2  8762  zorn2lem6  8812  grudomon  9124  indpi  9214  genpnmax  9314  reclem3pr  9356  reclem4pr  9357  suplem1pr  9359  supsrlem  9417  dedekind  9673  lemul12b  10334  fimaxre  10424  lbreu  10427  supmullem2  10444  cju  10466  nnind  10488  uz11  11041  xrre2  11310  qbtwnre  11337  xrsupexmnf  11435  xrinfmexpnf  11436  ico0  11514  ioc0  11515  ssfzoulel  11824  swrdccatin2  12642  coss12d  12829  sqrlem6  13102  o1lo1  13381  ruclem9  13992  isprm3  14247  eulerthlem2  14333  prmdiveq  14337  ramub2  14553  cictr  15230  joinfval  15767  meetfval  15781  clatl  15882  lubun  15889  ipodrsima  15931  dirtr  16002  mulgpropd  16311  dprdss  17208  subrgdvds  17575  dmatsubcl  19104  scmatcrng  19127  epttop  19614  cnpresti  19894  cnprest  19895  lmmo  19986  1stcrest  20058  lly1stc  20101  txcnp  20225  addcnlem  21472  caussi  21840  bcthlem5  21871  ovollb2lem  22003  voliunlem1  22064  ioombl1lem4  22075  rolle  22495  c1lip1  22502  c1lip3  22504  ulmval  22879  sqf11  23549  fsumvma  23624  dchrelbas3  23649  brbtwn2  24350  axeuclidlem  24407  axcontlem9  24417  axcontlem10  24418  usgra2adedgspthlem1  24753  usgra2adedgwlkon  24757  usgra2wlkspthlem2  24762  constr3trllem2  24793  4cycl4v4e  24808  4cycl4dv  24809  usg2wlkonot  25025  usg2wotspth  25026  eupai  25109  2pthfrgrarn2  25152  frgranbnb  25162  subgoablo  25451  nmcvcn  25743  sspmval  25784  sspival  25789  sspimsval  25791  sspph  25908  shsubcl  26276  shorth  26351  5oalem6  26715  strlem1  27306  atexch  27437  cdj3i  27497  xrge0infss  27760  xrofsup  27765  ishashinf  27789  nnindf  27793  cnre2csqima  28078  erdszelem9  28868  erdsze2lem2  28873  ss2mcls  29153  funpsstri  29397  dfon2lem4  29419  dfon2  29425  trpredrec  29522  frmin  29523  wfrlem4  29547  wsuclem  29582  frrlem4  29591  nocvxminlem  29651  nocvxmin  29652  nofulllem5  29667  elfuns  29754  btwnswapid  29856  ifscgr  29883  hilbert1.2  29994  wl-mo3t  30222  supadd  30243  ltflcei  30244  tan2h  30248  mblfinlem3  30254  elicc3  30337  tailfb  30397  fzmul  30435  metf1o  30450  ismtycnv  30500  ismtyres  30506  crngohomfo  30605  prtlem50  30790  iocinico  31383  pm11.59  31501  infrglb  31785  afvres  32458  usgvad2edg  32764  rhmsscrnghm  33069  ply1mulgsumlem1  33221  fldivexpfllog2  33421  hlhgt2  35561  hl2at  35577  2llnjN  35739  2lplnj  35792  linepsubN  35924  cdlemg33b0  36875  dvh3dim3N  37624  mapdh9a  37965
  Copyright terms: Public domain W3C validator