Theorem anim2d 567

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 25	. 2 |- ( ph -> ( th -> th ) )
2		anim1d.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	anim12d 565	1 |- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  eleq2d  2490  moeq3  3245  ssel  3455  sscon  3596  uniss  4234  trel3  4519  ssopab2  4738  coss1  5001  fununi  5658  imadif  5667  fss  5745  ssimaex  5937  opabbrexOLD  6339  ssoprab2  6352  poxp  6910  soxp  6911  pmss12g  7497  ss2ixp  7534  xpdom2  7664  fisup2g  7981  fisupcl  7982  inf3lem1  8124  epfrs  8205  cfub  8668  cflm  8669  fin23lem34  8765  isf32lem2  8773  axcc4  8858  domtriomlem  8861  ltexprlem3  9452  nnunb  10854  indstr  11216  qbtwnxr  11482  qsqueeze  11483  xrsupsslem  11581  xrinfmsslem  11582  ioc0  11672  climshftlem  13605  o1rlimmul  13649  ramub2  14923  monmat2matmon  19772  tgcl  19909  neips  20053  ssnei2  20056  tgcnp  20193  cnpnei  20204  cnpco  20207  hauscmplem  20345  hauscmp  20346  llyss  20418  nllyss  20419  lfinun  20464  kgen2ss  20494  txcnpi  20547  txcmplem1  20580  fgss  20812  cnpflf2  20939  fclsss1  20961  fclscf  20964  alexsubALT  20990  cnextcn  21006  tsmsxp  21093  mopni3  21433  psmetutop  21506  iscau4  22135  caussi  22153  ovolgelb  22307  mbfi1flim  22555  ellimc3  22708  lhop1  22840  tgbtwndiff  24410  axcontlem4  24840  iswlkg  25094  sspmval  26214  sspival  26219  shmodsi  26874  atcvat4i  27882  cdj3lem2b  27922  ifeqeqx  27994  acunirnmpt  28098  crefss  28512  issgon  28781  cvmlift2lem12  29822  ss2mcls  29991  poseq  30275  btwndiff  30576  seglecgr12im  30659  fnessref  30795  waj-ax  30856  lukshef-ax2  30857  icorempt2  31485  tan2h  31641  poimirlem31  31675  poimir  31677  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  cvrat4  32717  athgt  32730  ps-2  32752  paddss1  33091  paddss2  33092  cdlemg33b0  33977  cdlemg33a  33982  dihjat1lem  34705  fphpdo  35369  irrapxlem2  35377  pell14qrss1234  35412  pell1qrss14  35424  acongtr  35538  ax6e2eq  36565  islptre  37275  limccog  37276