Theorem anim1d 566

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  pm3.45  842  exdistrf  2134  2ax6elem  2248  mopick2  2339  ssrexf  3524  ssrexv  3526  ssdif  3600  ssrin  3687  reupick  3757  disjss1  4400  copsexg  4706  po3nr  4788  frss  4820  coss2  5010  ordsssuc2  5530  fununi  5667  dffv2  5955  extmptsuppeq  6951  onfununi  7072  oaass  7274  ssnnfi  7801  fiint  7858  fiss  7948  wemapsolem  8075  tcss  8237  ac6s  8922  reclem2pr  9481  qbtwnxr  11501  ico0  11690  icoshft  11762  2ffzeq  11918  clsslem  13049  r19.2uz  13415  infpn2  14857  prmgaplem4  15024  fthres2  15837  ablfacrplem  17698  monmat2matmon  19847  neiss  20124  uptx  20639  txcn  20640  nrmr0reg  20763  cnpflfi  21013  cnextcn  21081  caussi  22266  ovolsslem  22436  tgtrisegint  24542  inagswap  24879  cycliscrct  25357  numclwwlkovgelim  25816  shorth  26947  fmptss  28280  ordtconlem1  28739  omsmon  29135  omssubadd  29137  omsmonOLD  29139  omssubaddOLD  29141  mclsax  30216  poseq  30499  nodenselem5  30580  trisegint  30801  segcon2  30878  opnrebl2  30983  poimirlem30  31935  itg2addnclem  31958  itg2addnclem2  31959  fdc1  32040  totbndss  32074  ablo4pnp  32143  keridl  32230  dib2dim  34781  dih2dimbALTN  34783  dvh1dim  34980  mapdpglem2  35211  pell14qrss1234  35673  pell1qrss14  35685  rmxycomplete  35736  lnr2i  35946  rp-fakeanorass  36128  isprm7  36631  rfcnnnub  37331  nnsum4primes4  38755  nnsum4primesprm  38757  nnsum4primesgbe  38759  nnsum4primesle9  38761  propeqop  38866  2ffzoeq  38919