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

Theorem anim1d 564
 Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
anim1d.1
Assertion
Ref Expression
anim1d

Proof of Theorem anim1d
StepHypRef Expression
1 anim1d.1 . 2
2 idd 24 . 2
31, 2anim12d 563 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  pm3.45  834  exdistrf  2075  2ax6elem  2193  mopick2  2362  ssrexv  3564  ssdif  3638  ssrin  3722  reupick  3781  disjss1  4428  copsexg  4737  copsexgOLD  4738  po3nr  4819  frss  4851  ordsssuc2  4971  coss2  5164  fununi  5659  dffv2  5946  extmptsuppeq  6943  onfununi  7031  oaass  7229  ssnnfi  7759  fiint  7817  fiss  7904  wemapsolem  7996  tcss  8196  ac6s  8885  reclem2pr  9447  qbtwnxr  11428  ico0  11604  icoshft  11671  2ffzeq  11823  r19.2uz  13184  infpn2  14431  fthres2  15301  ablfacrplem  17116  monmat2matmon  19325  neiss  19610  uptx  20126  txcn  20127  nrmr0reg  20250  cnpflfi  20500  cnextcn  20567  caussi  21736  ovolsslem  21895  tgtrisegint  23890  cycliscrct  24630  numclwwlkovgelim  25089  shorth  26213  ordtconlem1  27906  omsmon  28267  mclsax  28929  poseq  29333  nodenselem5  29445  trisegint  29678  segcon2  29755  itg2addnclem  30066  itg2addnclem2  30067  opnrebl2  30139  fdc1  30239  totbndss  30273  ablo4pnp  30342  keridl  30429  pell14qrss1234  30792  pell1qrss14  30804  rmxycomplete  30853  lnr2i  31065  isprm7  31192  ssrexf  31388  rfcnnnub  31411  2ffzoeq  32341  dib2dim  36970  dih2dimbALTN  36972  dvh1dim  37169  mapdpglem2  37400  rp-fakeanorass  37737 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
 Copyright terms: Public domain W3C validator