Theorem anim2d 565

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.)

Hypothesis

Ref	Expression
anim1d.1

Assertion

Ref	Expression
anim2d

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 24	. 2
2		anim1d.1	. 2
3	1, 2	anim12d 563	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  eleq2d  2527  moeq3  3276  ssel  3497  sscon  3637  uniss  4270  trel3  4553  copsexgOLD  4738  ssopab2  4778  coss1  5163  fununi  5659  imadif  5668  fss  5744  ssimaex  5938  opabbrexOLD  6340  ssoprab2  6353  poxp  6912  soxp  6913  pmss12g  7465  ss2ixp  7502  xpdom2  7632  fisup2g  7947  fisupcl  7948  inf3lem1  8066  epfrs  8183  cfub  8650  cflm  8651  fin23lem34  8747  isf32lem2  8755  axcc4  8840  domtriomlem  8843  ltexprlem3  9437  nnunb  10816  indstr  11179  qbtwnxr  11428  qsqueeze  11429  xrsupsslem  11527  xrinfmsslem  11528  ioc0  11605  climshftlem  13397  o1rlimmul  13441  ramub2  14532  monmat2matmon  19325  tgcl  19471  neips  19614  ssnei2  19617  tgcnp  19754  cnpnei  19765  cnpco  19768  hauscmplem  19906  hauscmp  19907  llyss  19980  nllyss  19981  lfinun  20026  kgen2ss  20056  txcnpi  20109  txcmplem1  20142  fgss  20374  cnpflf2  20501  fclsss1  20523  fclscf  20526  alexsubALT  20551  cnextcn  20567  tsmsxp  20657  mopni3  20997  metutopOLD  21085  psmetutop  21086  iscau4  21718  caussi  21736  ovolgelb  21891  mbfi1flim  22130  ellimc3  22283  lhop1  22415  tgbtwndiff  23897  axcontlem4  24270  iswlkg  24524  sspmval  25646  sspival  25651  shmodsi  26307  atcvat4i  27316  cdj3lem2b  27356  ifeqeqx  27419  crefss  27852  issgon  28123  cvmlift2lem12  28759  ss2mcls  28928  poseq  29333  btwndiff  29677  seglecgr12im  29760  waj-ax  29879  lukshef-ax2  29880  tan2h  30047  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  fnessref  30175  fphpdo  30751  irrapxlem2  30759  pell14qrss1234  30792  pell1qrss14  30804  acongtr  30916  islptre  31625  limccog  31626  ax6e2eq  33330  cvrat4  35167  athgt  35180  ps-2  35202  paddss1  35541  paddss2  35542  cdlemg33b0  36427  cdlemg33a  36432  dihjat1lem  37155

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