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:  moeq3  3141  ssel  3355  sscon  3495  uniss  4117  trel3  4398  copsexgOLD  4582  ssopab2  4619  coss1  5000  fununi  5489  imadif  5498  fss  5572  ssimaex  5761  opabbrex  6135  ssoprab2  6147  poxp  6689  soxp  6690  pmss12g  7244  ss2ixp  7281  xpdom2  7411  fisup2g  7721  fisupcl  7722  inf3lem1  7839  epfrs  7956  cfub  8423  cflm  8424  fin23lem34  8520  isf32lem2  8528  axcc4  8613  domtriomlem  8616  ltexprlem3  9212  nnunb  10580  indstr  10928  qbtwnxr  11175  qsqueeze  11176  xrsupsslem  11274  xrinfmsslem  11275  ioc0  11352  climshftlem  13057  o1rlimmul  13101  ramub2  14080  tgcl  18579  neips  18722  ssnei2  18725  tgcnp  18862  cnpnei  18873  cnpco  18876  hauscmplem  19014  hauscmp  19015  llyss  19088  nllyss  19089  kgen2ss  19133  txcnpi  19186  txcmplem1  19219  fgss  19451  cnpflf2  19578  fclsss1  19600  fclscf  19603  alexsubALT  19628  cnextcn  19644  tsmsxp  19734  mopni3  20074  metutopOLD  20162  psmetutop  20163  iscau4  20795  caussi  20813  ovolgelb  20968  mbfi1flim  21206  ellimc3  21359  lhop1  21491  tgbtwndiff  22964  axcontlem4  23218  sspmval  24136  sspival  24141  shmodsi  24797  atcvat4i  25806  cdj3lem2b  25846  ifeqeqx  25907  issgon  26571  cvmlift2lem12  27208  poseq  27719  btwndiff  28063  seglecgr12im  28146  waj-ax  28265  lukshef-ax2  28266  tan2h  28429  mblfinlem3  28435  mblfinlem4  28436  ismblfin  28437  fnessref  28570  fphpdo  29161  irrapxlem2  29169  pell14qrss1234  29202  pell1qrss14  29214  acongtr  29326  iswlkg  30290  ax6e2eq  31271  cvrat4  33092  athgt  33105  ps-2  33127  paddss1  33466  paddss2  33467  cdlemg33b0  34350  cdlemg33a  34355  dihjat1lem  35078