Theorem anim2d 568

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 566	1 |- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  eleq2dOLD  2514  moeq3  3214  ssel  3425  sscon  3566  uniss  4218  trel3  4504  ssopab2  4726  coss1  4989  fununi  5647  imadif  5656  fss  5735  ssimaex  5928  opabbrexOLD  6331  ssoprab2  6344  poxp  6905  soxp  6906  pmss12g  7495  ss2ixp  7532  xpdom2  7664  fisup2g  7981  fisupcl  7982  fiinf2g  8013  inf3lem1  8130  epfrs  8212  cfub  8676  cflm  8677  fin23lem34  8773  isf32lem2  8781  axcc4  8866  domtriomlem  8869  ltexprlem3  9460  nnunb  10862  indstr  11224  qbtwnxr  11490  qsqueeze  11491  xrsupsslem  11589  xrinfmsslem  11590  ioc0  11680  climshftlem  13631  o1rlimmul  13675  ramub2  14964  monmat2matmon  19841  tgcl  19978  neips  20122  ssnei2  20125  tgcnp  20262  cnpnei  20273  cnpco  20276  hauscmplem  20414  hauscmp  20415  llyss  20487  nllyss  20488  lfinun  20533  kgen2ss  20563  txcnpi  20616  txcmplem1  20649  fgss  20881  cnpflf2  21008  fclsss1  21030  fclscf  21033  alexsubALT  21059  cnextcn  21075  tsmsxp  21162  mopni3  21502  psmetutop  21575  iscau4  22242  caussi  22260  ovolgelb  22426  mbfi1flim  22674  ellimc3  22827  lhop1  22959  tgbtwndiff  24543  axcontlem4  24990  iswlkg  25245  sspmval  26365  sspival  26370  shmodsi  27035  atcvat4i  28043  cdj3lem2b  28083  ifeqeqx  28151  acunirnmpt  28254  xrge0infss  28333  crefss  28669  issgon  28938  cvmlift2lem12  30030  ss2mcls  30199  poseq  30484  btwndiff  30787  seglecgr12im  30870  fnessref  31006  waj-ax  31067  lukshef-ax2  31068  icorempt2  31747  finxpreclem1  31774  tan2h  31930  poimirlem31  31964  poimir  31966  mblfinlem3  31972  mblfinlem4  31973  ismblfin  31974  cvrat4  33002  athgt  33015  ps-2  33037  paddss1  33376  paddss2  33377  cdlemg33b0  34262  cdlemg33a  34267  dihjat1lem  34990  fphpdo  35654  irrapxlem2  35661  pell14qrss1234  35696  pell1qrss14  35708  acongtr  35822  ax6e2eq  36918  islptre  37693  limccog  37694