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  2942  ssel  3174  sscon  3310  uniss  3848  trel3  4121  copsexg  4252  ssopab2  4290  coss1  4839  fununi  5316  imadif  5327  fss  5397  ssimaex  5584  ssoprab2  5904  poxp  6227  soxp  6228  tfrlem1  6391  pmss12g  6794  ss2ixp  6829  xpdom2  6957  fisup2g  7217  fisupcl  7218  inf3lem1  7329  epfrs  7413  cfub  7875  cflm  7876  fin23lem34  7972  isf32lem2  7980  axcc4  8065  domtriomlem  8068  ltexprlem3  8662  nnunb  9961  indstr  10287  qbtwnxr  10527  qsqueeze  10528  xrsupsslem  10625  xrinfmsslem  10626  ioc0  10703  climshftlem  12048  o1rlimmul  12092  ramub2  13061  tgcl  16707  neips  16850  ssnei2  16853  tgcnp  16983  cnpnei  16993  cnpco  16996  hauscmplem  17133  hauscmp  17134  llyss  17205  nllyss  17206  kgen2ss  17250  txcnpi  17302  txcmplem1  17335  fgss  17568  cnpflf2  17695  fclsss1  17717  fclscf  17720  alexsubALT  17745  tsmsxp  17837  mopni3  18040  iscau4  18705  caussi  18723  ovolgelb  18839  mbfi1flim  19078  ellimc3  19229  lhop1  19361  sspmval  21309  sspival  21314  shmodsi  21968  atcvat4i  22977  cdj3lem2b  23017  ifeqeqx  23034  issgon  23484  cvmlift2lem12  23845  poseq  24253  axcontlem4  24595  btwndiff  24650  seglecgr12im  24733  waj-ax  24853  lukshef-ax2  24854  untind  25018  ssoprab2g  25032  exopcopn  25572  tethpnc2  26071  isibg2aa  26112  fnessref  26293  fphpdo  26900  irrapxlem2  26908  pell14qrss1234  26941  pell1qrss14  26953  acongtr  27065  climrec  27729  a9e2eq  28323  cvrat4  29632  athgt  29645  ps-2  29667  paddss1  30006  paddss2  30007  cdlemg33b0  30890  cdlemg33a  30895  dihjat1lem  31618
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