Theorem anim12d 563

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
anim12d.2

Assertion

Ref	Expression
anim12d

Proof of Theorem anim12d

Step	Hyp	Ref	Expression
1		anim12d.1	. 2
2		anim12d.2	. 2
3		idd 24	. 2
4	1, 2, 3	syl2and 483	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  anim1d  564  anim2d  565  prth  571  im2anan9  835  anim12dan  837  3anim123d  1306  mo3  2323  2euswap  2370  2moOLD  2374  ssunsn2  4189  disjiun  4442  soss  4823  wess  4871  ordtri3  4919  oneqmini  4934  frinxp  5070  trin2  5395  xp11  5447  funss  5611  fun  5753  fvcofneq  6039  dff13  6166  f1eqcocnv  6204  isores3  6231  isosolem  6243  isowe2  6246  ordom  6709  f1oweALT  6784  f1o2ndf1  6908  tposfn2  6996  tposf1o2  7000  smo11  7054  tz7.48lem  7125  om00  7243  omsmo  7322  ixpfi2  7838  elfiun  7910  supmo  7932  alephord  8477  cardaleph  8491  dfac5  8530  fin1a2lem9  8809  axdc3lem2  8852  zorn2lem6  8902  grudomon  9216  indpi  9306  genpnmax  9406  reclem3pr  9448  reclem4pr  9449  suplem1pr  9451  supsrlem  9509  dedekind  9765  lemul12b  10424  fimaxre  10515  lbreu  10518  supmullem2  10535  cju  10557  nnind  10579  uz11  11132  xrre2  11400  qbtwnre  11427  xrsupexmnf  11525  xrinfmexpnf  11526  ico0  11604  ioc0  11605  ssfzoulel  11906  swrdnd  12657  swrdccatin2  12712  sqrlem6  13081  o1lo1  13360  ruclem9  13971  isprm3  14226  eulerthlem2  14312  prmdiveq  14316  ramub2  14532  joinfval  15631  meetfval  15645  clatl  15746  lubun  15753  ipodrsima  15795  dirtr  15866  mulgpropd  16175  dprdss  17076  subrgdvds  17443  dmatsubcl  19000  scmatcrng  19023  epttop  19510  cnpresti  19789  cnprest  19790  lmmo  19881  1stcrest  19954  lly1stc  19997  txcnp  20121  addcnlem  21368  caussi  21736  bcthlem5  21767  ovollb2lem  21899  voliunlem1  21960  ioombl1lem4  21971  rolle  22391  c1lip1  22398  c1lip3  22400  ulmval  22775  sqf11  23413  fsumvma  23488  dchrelbas3  23513  brbtwn2  24208  axeuclidlem  24265  axcontlem9  24275  axcontlem10  24276  usgra2adedgspthlem1  24611  usgra2adedgwlkon  24615  usgra2wlkspthlem2  24620  constr3trllem2  24651  4cycl4v4e  24666  4cycl4dv  24667  usg2wlkonot  24883  usg2wotspth  24884  eupai  24967  2pthfrgrarn2  25010  frgranbnb  25020  subgoablo  25313  nmcvcn  25605  sspmval  25646  sspival  25651  sspimsval  25653  sspph  25770  shsubcl  26138  shorth  26213  5oalem6  26577  strlem1  27169  atexch  27300  cdj3i  27360  xrge0infss  27580  xrofsup  27582  ishashinf  27606  nnindf  27610  cnre2csqima  27893  erdszelem9  28643  erdsze2lem2  28648  ss2mcls  28928  funpsstri  29195  dfon2lem4  29218  dfon2  29224  trpredrec  29321  frmin  29322  wfrlem4  29346  wsuclem  29381  frrlem4  29390  nocvxminlem  29450  nocvxmin  29451  nofulllem5  29466  elfuns  29565  btwnswapid  29667  ifscgr  29694  hilbert1.2  29805  wl-mo3t  30021  supadd  30042  ltflcei  30043  tan2h  30047  mblfinlem3  30053  elicc3  30135  tailfb  30195  fzmul  30233  metf1o  30248  ismtycnv  30298  ismtyres  30304  crngohomfo  30403  prtlem50  30588  iocinico  31179  pm11.59  31297  infrglb  31584  afvres  32257  usgvad2edg  32411  cictr  32589  rhmsscrnghm  32834  ply1mulgsumlem1  32986  hlhgt2  35113  hl2at  35129  2llnjN  35291  2lplnj  35344  linepsubN  35476  cdlemg33b0  36427  dvh3dim3N  37176  mapdh9a  37517  coss12d  37759

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 371