Theorem anim2d 560

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

Step	Hyp	Ref	Expression
1		idd 24	. 2 |- ( ph -> ( th -> th ) )
2		anim1d.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	anim12d 558	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:  moeq3  3125  ssel  3338  sscon  3478  uniss  4100  trel3  4381  copsexg  4564  copsexgOLD  4565  ssopab2  4603  coss1  4982  fununi  5472  imadif  5481  fss  5555  ssimaex  5744  opabbrex  6119  ssoprab2  6131  poxp  6673  soxp  6674  pmss12g  7227  ss2ixp  7264  xpdom2  7394  fisup2g  7704  fisupcl  7705  inf3lem1  7822  epfrs  7939  cfub  8406  cflm  8407  fin23lem34  8503  isf32lem2  8511  axcc4  8596  domtriomlem  8599  ltexprlem3  9194  nnunb  10562  indstr  10910  qbtwnxr  11157  qsqueeze  11158  xrsupsslem  11256  xrinfmsslem  11257  ioc0  11334  climshftlem  13035  o1rlimmul  13079  ramub2  14057  tgcl  18415  neips  18558  ssnei2  18561  tgcnp  18698  cnpnei  18709  cnpco  18712  hauscmplem  18850  hauscmp  18851  llyss  18924  nllyss  18925  kgen2ss  18969  txcnpi  19022  txcmplem1  19055  fgss  19287  cnpflf2  19414  fclsss1  19436  fclscf  19439  alexsubALT  19464  cnextcn  19480  tsmsxp  19570  mopni3  19910  metutopOLD  19998  psmetutop  19999  iscau4  20631  caussi  20649  ovolgelb  20804  mbfi1flim  21042  ellimc3  21195  lhop1  21327  tgbtwndiff  22840  axcontlem4  23035  sspmval  23953  sspival  23958  shmodsi  24614  atcvat4i  25623  cdj3lem2b  25663  ifeqeqx  25725  issgon  26419  cvmlift2lem12  27050  poseq  27560  btwndiff  27904  seglecgr12im  27987  waj-ax  28107  lukshef-ax2  28108  tan2h  28265  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  fnessref  28406  fphpdo  28998  irrapxlem2  29006  pell14qrss1234  29039  pell1qrss14  29051  acongtr  29163  iswlkg  30128  ax6e2eq  30964  cvrat4  32657  athgt  32670  ps-2  32692  paddss1  33031  paddss2  33032  cdlemg33b0  33915  cdlemg33a  33920  dihjat1lem  34643