Theorem anim1d 561

Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)

Hypothesis

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

Assertion

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

Proof of Theorem anim1d

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

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:  pm3.45  825  exdistrf  2030  2sb6rflem1  2162  mopick  2342  mopick2  2351  ssrexv  3414  ssdif  3488  ssrin  3572  reupick  3631  disjss1  4265  copsexg  4573  copsexgOLD  4574  po3nr  4651  frss  4683  ordsssuc2  4803  coss2  4992  fununi  5481  dffv2  5761  extmptsuppeq  6712  onfununi  6798  oaass  6996  ssnnfi  7528  fiint  7584  fiss  7670  wemapsolem  7760  tcss  7960  ac6s  8649  reclem2pr  9213  qbtwnxr  11166  ico0  11342  icoshft  11403  r19.2uz  12835  infpn2  13970  fthres2  14838  ablfacrplem  16556  neiss  18672  uptx  19157  txcn  19158  nrmr0reg  19281  cnpflfi  19531  cnextcn  19598  caussi  20767  ovolsslem  20926  tgtrisegint  22911  cycliscrct  23451  shorth  24633  ordtconlem1  26290  poseq  27643  nodenselem5  27755  trisegint  27988  segcon2  28065  itg2addnclem  28368  itg2addnclem2  28369  opnrebl2  28441  fdc1  28567  totbndss  28601  ablo4pnp  28670  keridl  28757  pell14qrss1234  29122  pell1qrss14  29134  rmxycomplete  29183  lnr2i  29397  ssrexf  29660  rfcnnnub  29683  2ffzeq  30129  2ffzoeq  30139  numclwwlkovgelim  30607  dib2dim  34610  dih2dimbALTN  34612  dvh1dim  34809  mapdpglem2  35040