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

Theorem anim2d 548
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 21 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 anim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2anim12d 546 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ( th 
/\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  moeq3  2955  ssel  3187  sscon  3323  uniss  3864  trel3  4137  copsexg  4268  ssopab2  4306  coss1  4855  fununi  5332  imadif  5343  fss  5413  ssimaex  5600  ssoprab2  5920  poxp  6243  soxp  6244  tfrlem1  6407  pmss12g  6810  ss2ixp  6845  xpdom2  6973  fisup2g  7233  fisupcl  7234  inf3lem1  7345  epfrs  7429  cfub  7891  cflm  7892  fin23lem34  7988  isf32lem2  7996  axcc4  8081  domtriomlem  8084  ltexprlem3  8678  nnunb  9977  indstr  10303  qbtwnxr  10543  qsqueeze  10544  xrsupsslem  10641  xrinfmsslem  10642  ioc0  10719  climshftlem  12064  o1rlimmul  12108  ramub2  13077  tgcl  16723  neips  16866  ssnei2  16869  tgcnp  16999  cnpnei  17009  cnpco  17012  hauscmplem  17149  hauscmp  17150  llyss  17221  nllyss  17222  kgen2ss  17266  txcnpi  17318  txcmplem1  17351  fgss  17584  cnpflf2  17711  fclsss1  17733  fclscf  17736  alexsubALT  17761  tsmsxp  17853  mopni3  18056  iscau4  18721  caussi  18739  ovolgelb  18855  mbfi1flim  19094  ellimc3  19245  lhop1  19377  sspmval  21325  sspival  21330  shmodsi  21984  atcvat4i  22993  cdj3lem2b  23033  ifeqeqx  23050  issgon  23499  cvmlift2lem12  23860  poseq  24324  axcontlem4  24667  btwndiff  24722  seglecgr12im  24805  waj-ax  24925  lukshef-ax2  24926  untind  25121  ssoprab2g  25135  exopcopn  25675  tethpnc2  26174  isibg2aa  26215  fnessref  26396  fphpdo  27003  irrapxlem2  27011  pell14qrss1234  27044  pell1qrss14  27056  acongtr  27168  climrec  27832  opabbrex  28191  a9e2eq  28622  cvrat4  30254  athgt  30267  ps-2  30289  paddss1  30628  paddss2  30629  cdlemg33b0  31512  cdlemg33a  31517  dihjat1lem  32240
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 177  df-an 360
  Copyright terms: Public domain W3C validator