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

Theorem anim2d 549
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 22 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 anim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2anim12d 547 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ( th 
/\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  moeq3  3047  ssel  3278  sscon  3417  uniss  3971  trel3  4244  copsexg  4376  ssopab2  4414  coss1  4961  fununi  5450  imadif  5461  fss  5532  ssimaex  5720  opabbrex  6050  ssoprab2  6062  poxp  6387  soxp  6388  tfrlem1  6565  pmss12g  6969  ss2ixp  7004  xpdom2  7132  fisup2g  7397  fisupcl  7398  inf3lem1  7509  epfrs  7593  cfub  8055  cflm  8056  fin23lem34  8152  isf32lem2  8160  axcc4  8245  domtriomlem  8248  ltexprlem3  8841  nnunb  10142  indstr  10470  qbtwnxr  10711  qsqueeze  10712  xrsupsslem  10810  xrinfmsslem  10811  ioc0  10888  climshftlem  12288  o1rlimmul  12332  ramub2  13302  tgcl  16950  neips  17093  ssnei2  17096  tgcnp  17232  cnpnei  17243  cnpco  17246  hauscmplem  17384  hauscmp  17385  llyss  17456  nllyss  17457  kgen2ss  17501  txcnpi  17554  txcmplem1  17587  fgss  17819  cnpflf2  17946  fclsss1  17968  fclscf  17971  alexsubALT  17996  cnextcn  18012  tsmsxp  18098  mopni3  18407  metutop  18480  iscau4  19096  caussi  19114  ovolgelb  19236  mbfi1flim  19475  ellimc3  19626  lhop1  19758  sspmval  22073  sspival  22078  shmodsi  22732  atcvat4i  23741  cdj3lem2b  23781  ifeqeqx  23838  issgon  24295  cvmlift2lem12  24773  poseq  25270  axcontlem4  25613  btwndiff  25668  seglecgr12im  25751  waj-ax  25871  lukshef-ax2  25872  fnessref  26057  fphpdo  26562  irrapxlem2  26570  pell14qrss1234  26603  pell1qrss14  26615  acongtr  26727  a9e2eq  27980  cvrat4  29608  athgt  29621  ps-2  29643  paddss1  29982  paddss2  29983  cdlemg33b0  30866  cdlemg33a  30871  dihjat1lem  31594
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator