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

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  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
anim2d  |-  ( ph  ->  ( ( th  /\  ps )  ->  ( th 
/\  ch ) ) )

Proof of Theorem anim2d
StepHypRef Expression
1 idd 24 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 anim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2anim12d 563 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ( th 
/\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  eleq2d  2537  moeq3  3280  ssel  3498  sscon  3638  uniss  4266  trel3  4548  copsexgOLD  4733  ssopab2  4773  coss1  5156  fununi  5652  imadif  5661  fss  5737  ssimaex  5930  opabbrex  6322  ssoprab2  6335  poxp  6892  soxp  6893  pmss12g  7442  ss2ixp  7479  xpdom2  7609  fisup2g  7922  fisupcl  7923  inf3lem1  8041  epfrs  8158  cfub  8625  cflm  8626  fin23lem34  8722  isf32lem2  8730  axcc4  8815  domtriomlem  8818  ltexprlem3  9412  nnunb  10787  indstr  11146  qbtwnxr  11395  qsqueeze  11396  xrsupsslem  11494  xrinfmsslem  11495  ioc0  11572  climshftlem  13356  o1rlimmul  13400  ramub2  14387  monmat2matmon  19092  tgcl  19237  neips  19380  ssnei2  19383  tgcnp  19520  cnpnei  19531  cnpco  19534  hauscmplem  19672  hauscmp  19673  llyss  19746  nllyss  19747  kgen2ss  19791  txcnpi  19844  txcmplem1  19877  fgss  20109  cnpflf2  20236  fclsss1  20258  fclscf  20261  alexsubALT  20286  cnextcn  20302  tsmsxp  20392  mopni3  20732  metutopOLD  20820  psmetutop  20821  iscau4  21453  caussi  21471  ovolgelb  21626  mbfi1flim  21865  ellimc3  22018  lhop1  22150  tgbtwndiff  23625  axcontlem4  23946  iswlkg  24200  sspmval  25322  sspival  25327  shmodsi  25983  atcvat4i  26992  cdj3lem2b  27032  ifeqeqx  27093  issgon  27763  cvmlift2lem12  28399  poseq  28910  btwndiff  29254  seglecgr12im  29337  waj-ax  29456  lukshef-ax2  29457  tan2h  29624  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  fnessref  29765  fphpdo  30355  irrapxlem2  30363  pell14qrss1234  30396  pell1qrss14  30408  acongtr  30520  islptre  31161  limccog  31162  ax6e2eq  32410  cvrat4  34239  athgt  34252  ps-2  34274  paddss1  34613  paddss2  34614  cdlemg33b0  35497  cdlemg33a  35502  dihjat1lem  36225
  Copyright terms: Public domain W3C validator