Theorem anim1d 548

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  pm3.45  808  ax12olem2OLD  1978  exdistrf  2028  mopick2  2321  ssrexv  3368  ssdif  3442  ssrin  3526  reupick  3585  disjss1  4148  copsexg  4402  po3nr  4477  frss  4509  ordsssuc2  4629  coss2  4988  fununi  5476  dffv2  5755  onfununi  6562  oaass  6763  ssnnfi  7287  fiint  7342  fiss  7387  wemapso2lem  7475  cantnfreslem  7587  tcss  7639  ac6s  8320  reclem2pr  8881  qbtwnxr  10742  ico0  10918  icoshft  10975  r19.2uz  12110  infpn2  13236  fthres2  14084  ablfacrplem  15578  neiss  17128  uptx  17610  txcn  17611  nrmr0reg  17734  cnpflfi  17984  cnextcn  18051  caussi  19203  ovolsslem  19333  cycliscrct  21570  shorth  22750  poseq  25467  nodenselem5  25553  trisegint  25866  segcon2  25943  itg2addnclem  26155  itg2addnclem2  26156  opnrebl2  26214  fdc1  26340  totbndss  26376  ablo4pnp  26445  keridl  26532  pell14qrss1234  26809  pell1qrss14  26821  rmxycomplete  26870  lnr2i  27188  ssrexf  27551  rfcnnnub  27574  ax12olem2wAUX7  29162  exdistrfNEW7  29211  ax12olem2OLD7  29390  dib2dim  31726  dih2dimbALTN  31728  dvh1dim  31925  mapdpglem2  32156

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361