Theorem anim1d 572

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  pm3.45  849  exdistrf  2168  2ax6elem  2279  mopick2  2370  ssrexf  3460  ssrexv  3462  ssdif  3536  ssrin  3625  reupick  3695  disjss1  4351  copsexg  4660  po3nr  4747  frss  4779  coss2  4969  ordsssuc2  5490  fununi  5631  dffv2  5922  extmptsuppeq  6927  onfununi  7047  oaass  7249  ssnnfi  7778  fiint  7835  fiss  7925  wemapsolem  8052  tcss  8215  ac6s  8901  reclem2pr  9460  qbtwnxr  11483  ico0  11672  icoshft  11745  2ffzeq  11903  clsslem  13059  r19.2uz  13425  infpn2  14868  prmgaplem4  15035  fthres2  15848  ablfacrplem  17709  monmat2matmon  19859  neiss  20136  uptx  20651  txcn  20652  nrmr0reg  20775  cnpflfi  21025  cnextcn  21093  caussi  22278  ovolsslem  22448  tgtrisegint  24555  inagswap  24892  cycliscrct  25370  numclwwlkovgelim  25829  shorth  26960  fmptss  28285  ordtconlem1  28737  omsmon  29132  omssubadd  29134  omsmonOLD  29136  omssubaddOLD  29138  mclsax  30213  poseq  30497  nodenselem5  30580  trisegint  30801  segcon2  30878  opnrebl2  30983  poimirlem30  31972  itg2addnclem  31995  itg2addnclem2  31996  fdc1  32077  totbndss  32111  ablo4pnp  32180  keridl  32267  dib2dim  34813  dih2dimbALTN  34815  dvh1dim  35012  mapdpglem2  35243  pell14qrss1234  35704  pell1qrss14  35716  rmxycomplete  35767  lnr2i  35977  rp-fakeanorass  36159  isprm7  36661  rfcnnnub  37354  nnsum4primes4  38975  nnsum4primesprm  38977  nnsum4primesgbe  38979  nnsum4primesle9  38981  propeqop  39092  2ffzoeq  39158  cyclisCrct  39873