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  3103  ssel  3334  sscon  3473  uniss  4028  trel3  4302  copsexg  4434  ssopab2  4472  coss1  5019  fununi  5508  imadif  5519  fss  5590  ssimaex  5779  opabbrex  6109  ssoprab2  6121  poxp  6449  soxp  6450  tfrlem1  6627  pmss12g  7031  ss2ixp  7066  xpdom2  7194  fisup2g  7460  fisupcl  7461  inf3lem1  7572  epfrs  7656  cfub  8118  cflm  8119  fin23lem34  8215  isf32lem2  8223  axcc4  8308  domtriomlem  8311  ltexprlem3  8904  nnunb  10206  indstr  10534  qbtwnxr  10775  qsqueeze  10776  xrsupsslem  10874  xrinfmsslem  10875  ioc0  10952  climshftlem  12356  o1rlimmul  12400  ramub2  13370  tgcl  17022  neips  17165  ssnei2  17168  tgcnp  17305  cnpnei  17316  cnpco  17319  hauscmplem  17457  hauscmp  17458  llyss  17530  nllyss  17531  kgen2ss  17575  txcnpi  17628  txcmplem1  17661  fgss  17893  cnpflf2  18020  fclsss1  18042  fclscf  18045  alexsubALT  18070  cnextcn  18086  tsmsxp  18172  mopni3  18512  metutopOLD  18600  psmetutop  18601  iscau4  19220  caussi  19238  ovolgelb  19364  mbfi1flim  19603  ellimc3  19754  lhop1  19886  sspmval  22220  sspival  22225  shmodsi  22879  atcvat4i  23888  cdj3lem2b  23928  ifeqeqx  23989  issgon  24494  cvmlift2lem12  24989  poseq  25508  axcontlem4  25854  btwndiff  25909  seglecgr12im  25992  waj-ax  26112  lukshef-ax2  26113  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  fnessref  26310  fphpdo  26815  irrapxlem2  26823  pell14qrss1234  26856  pell1qrss14  26868  acongtr  26980  a9e2eq  28499  cvrat4  30079  athgt  30092  ps-2  30114  paddss1  30453  paddss2  30454  cdlemg33b0  31337  cdlemg33a  31342  dihjat1lem  32065
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