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

Theorem anim2d 550
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 23 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 anim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2anim12d 548 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ( th 
/\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  moeq3  3113  ssel  3344  sscon  3483  uniss  4038  trel3  4313  copsexg  4445  ssopab2  4483  coss1  5031  fununi  5520  imadif  5531  fss  5602  ssimaex  5791  opabbrex  6121  ssoprab2  6133  poxp  6461  soxp  6462  tfrlem1  6639  pmss12g  7043  ss2ixp  7078  xpdom2  7206  fisup2g  7474  fisupcl  7475  inf3lem1  7586  epfrs  7670  cfub  8134  cflm  8135  fin23lem34  8231  isf32lem2  8239  axcc4  8324  domtriomlem  8327  ltexprlem3  8920  nnunb  10222  indstr  10550  qbtwnxr  10791  qsqueeze  10792  xrsupsslem  10890  xrinfmsslem  10891  ioc0  10968  climshftlem  12373  o1rlimmul  12417  ramub2  13387  tgcl  17039  neips  17182  ssnei2  17185  tgcnp  17322  cnpnei  17333  cnpco  17336  hauscmplem  17474  hauscmp  17475  llyss  17547  nllyss  17548  kgen2ss  17592  txcnpi  17645  txcmplem1  17678  fgss  17910  cnpflf2  18037  fclsss1  18059  fclscf  18062  alexsubALT  18087  cnextcn  18103  tsmsxp  18189  mopni3  18529  metutopOLD  18617  psmetutop  18618  iscau4  19237  caussi  19255  ovolgelb  19381  mbfi1flim  19618  ellimc3  19771  lhop1  19903  sspmval  22237  sspival  22242  shmodsi  22896  atcvat4i  23905  cdj3lem2b  23945  ifeqeqx  24006  issgon  24511  cvmlift2lem12  25006  poseq  25533  axcontlem4  25911  btwndiff  25966  seglecgr12im  26049  waj-ax  26169  lukshef-ax2  26170  tan2h  26252  mblfinlem3  26257  mblfinlem4  26258  ismblfin  26259  fnessref  26387  fphpdo  26892  irrapxlem2  26900  pell14qrss1234  26933  pell1qrss14  26945  acongtr  27057  iswlkg  28338  a9e2eq  28718  cvrat4  30314  athgt  30327  ps-2  30349  paddss1  30688  paddss2  30689  cdlemg33b0  31572  cdlemg33a  31577  dihjat1lem  32300
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 179  df-an 362
  Copyright terms: Public domain W3C validator