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  830  exdistrf  2034  2ax6elem  2165  mopick  2347  mopick2  2356  ssrexv  3520  ssdif  3594  ssrin  3678  reupick  3737  disjss1  4371  copsexg  4679  copsexgOLD  4680  po3nr  4758  frss  4790  ordsssuc2  4910  coss2  5099  fununi  5587  dffv2  5868  extmptsuppeq  6818  onfununi  6907  oaass  7105  ssnnfi  7638  fiint  7694  fiss  7780  wemapsolem  7870  tcss  8070  ac6s  8759  reclem2pr  9323  qbtwnxr  11276  ico0  11452  icoshft  11519  r19.2uz  12952  infpn2  14087  fthres2  14956  ablfacrplem  16683  neiss  18840  uptx  19325  txcn  19326  nrmr0reg  19449  cnpflfi  19699  cnextcn  19766  caussi  20935  ovolsslem  21094  tgtrisegint  23082  cycliscrct  23663  shorth  24845  ordtconlem1  26494  omsmon  26850  poseq  27853  nodenselem5  27965  trisegint  28198  segcon2  28275  itg2addnclem  28586  itg2addnclem2  28587  opnrebl2  28659  fdc1  28785  totbndss  28819  ablo4pnp  28888  keridl  28975  pell14qrss1234  29340  pell1qrss14  29352  rmxycomplete  29401  lnr2i  29615  ssrexf  29878  rfcnnnub  29901  2ffzeq  30347  2ffzoeq  30357  numclwwlkovgelim  30825  monmat2matmon  31291  dib2dim  35207  dih2dimbALTN  35209  dvh1dim  35406  mapdpglem2  35637