Theorem anim2d 565

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.)

Hypothesis

Ref	Expression
anim1d.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
anim2d	|- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 24	. 2 |- ( ph -> ( th -> th ) )
2		anim1d.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	anim12d 563	1 |- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  eleq2d  2527  moeq3  3276  ssel  3493  sscon  3634  uniss  4272  trel3  4558  copsexgOLD  4742  ssopab2  4782  coss1  5168  fununi  5660  imadif  5669  fss  5745  ssimaex  5938  opabbrexOLD  6339  ssoprab2  6352  poxp  6911  soxp  6912  pmss12g  7464  ss2ixp  7501  xpdom2  7631  fisup2g  7944  fisupcl  7945  inf3lem1  8062  epfrs  8179  cfub  8646  cflm  8647  fin23lem34  8743  isf32lem2  8751  axcc4  8836  domtriomlem  8839  ltexprlem3  9433  nnunb  10812  indstr  11175  qbtwnxr  11424  qsqueeze  11425  xrsupsslem  11523  xrinfmsslem  11524  ioc0  11601  climshftlem  13408  o1rlimmul  13452  ramub2  14543  monmat2matmon  19451  tgcl  19597  neips  19740  ssnei2  19743  tgcnp  19880  cnpnei  19891  cnpco  19894  hauscmplem  20032  hauscmp  20033  llyss  20105  nllyss  20106  lfinun  20151  kgen2ss  20181  txcnpi  20234  txcmplem1  20267  fgss  20499  cnpflf2  20626  fclsss1  20648  fclscf  20651  alexsubALT  20676  cnextcn  20692  tsmsxp  20782  mopni3  21122  metutopOLD  21210  psmetutop  21211  iscau4  21843  caussi  21861  ovolgelb  22016  mbfi1flim  22255  ellimc3  22408  lhop1  22540  tgbtwndiff  24022  axcontlem4  24396  iswlkg  24650  sspmval  25772  sspival  25777  shmodsi  26433  atcvat4i  27442  cdj3lem2b  27482  ifeqeqx  27552  acunirnmpt  27647  crefss  28005  issgon  28284  cvmlift2lem12  28934  ss2mcls  29103  poseq  29507  btwndiff  29839  seglecgr12im  29922  waj-ax  30041  lukshef-ax2  30042  tan2h  30209  mblfinlem3  30215  mblfinlem4  30216  ismblfin  30217  fnessref  30337  fphpdo  30913  irrapxlem2  30921  pell14qrss1234  30954  pell1qrss14  30966  acongtr  31078  islptre  31786  limccog  31787  ax6e2eq  33431  cvrat4  35268  athgt  35281  ps-2  35303  paddss1  35642  paddss2  35643  cdlemg33b0  36528  cdlemg33a  36533  dihjat1lem  37256