Theorem anim1d 564

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 563	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  832  exdistrf  2048  2ax6elem  2179  mopick  2361  mopick2  2370  ssrexv  3565  ssdif  3639  ssrin  3723  reupick  3782  disjss1  4423  copsexg  4732  copsexgOLD  4733  po3nr  4814  frss  4846  ordsssuc2  4966  coss2  5159  fununi  5654  dffv2  5940  extmptsuppeq  6924  onfununi  7012  oaass  7210  ssnnfi  7739  fiint  7797  fiss  7884  wemapsolem  7975  tcss  8175  ac6s  8864  reclem2pr  9426  qbtwnxr  11399  ico0  11575  icoshft  11642  2ffzeq  11791  r19.2uz  13147  infpn2  14290  fthres2  15159  ablfacrplem  16918  monmat2matmon  19120  neiss  19404  uptx  19889  txcn  19890  nrmr0reg  20013  cnpflfi  20263  cnextcn  20330  caussi  21499  ovolsslem  21658  tgtrisegint  23646  cycliscrct  24334  numclwwlkovgelim  24794  shorth  25917  ordtconlem1  27570  omsmon  27935  poseq  28938  nodenselem5  29050  trisegint  29283  segcon2  29360  itg2addnclem  29671  itg2addnclem2  29672  opnrebl2  29744  fdc1  29870  totbndss  29904  ablo4pnp  29973  keridl  30060  pell14qrss1234  30424  pell1qrss14  30436  rmxycomplete  30485  lnr2i  30697  isprm7  30823  ssrexf  30994  rfcnnnub  31017  2ffzoeq  31836  dib2dim  36058  dih2dimbALTN  36060  dvh1dim  36257  mapdpglem2  36488