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  834  exdistrf  2076  2ax6elem  2194  mopick2  2362  ssrexf  3559  ssrexv  3561  ssdif  3635  ssrin  3719  reupick  3789  disjss1  4433  copsexg  4741  copsexgOLD  4742  po3nr  4823  frss  4855  ordsssuc2  4975  coss2  5169  fununi  5660  dffv2  5946  extmptsuppeq  6942  onfununi  7030  oaass  7228  ssnnfi  7758  fiint  7815  fiss  7902  wemapsolem  7993  tcss  8192  ac6s  8881  reclem2pr  9443  qbtwnxr  11424  ico0  11600  icoshft  11667  2ffzeq  11820  r19.2uz  13196  infpn2  14443  fthres2  15348  ablfacrplem  17243  monmat2matmon  19452  neiss  19737  uptx  20252  txcn  20253  nrmr0reg  20376  cnpflfi  20626  cnextcn  20693  caussi  21862  ovolsslem  22021  tgtrisegint  24016  cycliscrct  24757  numclwwlkovgelim  25216  shorth  26340  fmptss  27670  ordtconlem1  28067  omsmon  28442  omssubadd  28444  mclsax  29126  poseq  29529  nodenselem5  29641  trisegint  29862  segcon2  29939  itg2addnclem  30250  itg2addnclem2  30251  opnrebl2  30323  fdc1  30423  totbndss  30457  ablo4pnp  30526  keridl  30613  pell14qrss1234  30975  pell1qrss14  30987  rmxycomplete  31036  lnr2i  31248  isprm7  31375  rfcnnnub  31593  2ffzoeq  32584  dib2dim  37092  dih2dimbALTN  37094  dvh1dim  37291  mapdpglem2  37522  rp-fakeanorass  37859