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

Theorem anim2d 560
Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-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 558 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:  moeq3  3125  ssel  3338  sscon  3478  uniss  4100  trel3  4381  copsexg  4564  copsexgOLD  4565  ssopab2  4603  coss1  4982  fununi  5472  imadif  5481  fss  5555  ssimaex  5744  opabbrex  6119  ssoprab2  6131  poxp  6673  soxp  6674  pmss12g  7227  ss2ixp  7264  xpdom2  7394  fisup2g  7704  fisupcl  7705  inf3lem1  7822  epfrs  7939  cfub  8406  cflm  8407  fin23lem34  8503  isf32lem2  8511  axcc4  8596  domtriomlem  8599  ltexprlem3  9194  nnunb  10562  indstr  10910  qbtwnxr  11157  qsqueeze  11158  xrsupsslem  11256  xrinfmsslem  11257  ioc0  11334  climshftlem  13035  o1rlimmul  13079  ramub2  14057  tgcl  18415  neips  18558  ssnei2  18561  tgcnp  18698  cnpnei  18709  cnpco  18712  hauscmplem  18850  hauscmp  18851  llyss  18924  nllyss  18925  kgen2ss  18969  txcnpi  19022  txcmplem1  19055  fgss  19287  cnpflf2  19414  fclsss1  19436  fclscf  19439  alexsubALT  19464  cnextcn  19480  tsmsxp  19570  mopni3  19910  metutopOLD  19998  psmetutop  19999  iscau4  20631  caussi  20649  ovolgelb  20804  mbfi1flim  21042  ellimc3  21195  lhop1  21327  tgbtwndiff  22840  axcontlem4  23035  sspmval  23953  sspival  23958  shmodsi  24614  atcvat4i  25623  cdj3lem2b  25663  ifeqeqx  25725  issgon  26419  cvmlift2lem12  27050  poseq  27560  btwndiff  27904  seglecgr12im  27987  waj-ax  28107  lukshef-ax2  28108  tan2h  28265  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  fnessref  28406  fphpdo  28998  irrapxlem2  29006  pell14qrss1234  29039  pell1qrss14  29051  acongtr  29163  iswlkg  30128  ax6e2eq  30964  cvrat4  32657  athgt  32670  ps-2  32692  paddss1  33031  paddss2  33032  cdlemg33b0  33915  cdlemg33a  33920  dihjat1lem  34643
  Copyright terms: Public domain W3C validator