Theorem anim12i 338

Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)

Hypotheses

Ref	Expression
anim12i.1	|- ( ph -> ps )
anim12i.2	|- ( ch -> th )

Assertion

Ref	Expression
anim12i	|- ( ( ph /\ ch ) -> ( ps /\ th ) )

Proof of Theorem anim12i

Step	Hyp	Ref	Expression
1		anim12i.1	. 2 |- ( ph -> ps )
2		anim12i.2	. 2 |- ( ch -> th )
3		id 19	. 2 |- ( ( ps /\ th ) -> ( ps /\ th ) )
4	1, 2, 3	syl2an 289	1 |- ( ( ph /\ ch ) -> ( ps /\ th ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  anim12ci  339  anim1i  340  anim2i  342  anifpdc  992  hban  1593  sbimi  1810  spsbbi  1890  2exeu  2170  cgsex2g  2836  cgsex4g  2837  spc2egv  2893  spc2gv  2894  sseq2  3248  unssin  3443  uneqin  3455  undif3ss  3465  prneimg  3852  ssunieq  3921  iuneq1  3978  iuneq2  3981  copsex2t  4331  soeq2  4407  tpexg  4535  eldifpw  4568  iunpw  4571  peano5  4690  opbrop  4798  xpsspw  4831  coeq1  4879  coeq2  4880  cnveq  4896  dmeq  4923  sotri  5124  elxp4  5216  elxp5  5217  funun  5362  fununfun  5364  fundif  5365  funtp  5374  imain  5403  2elresin  5434  funssxp  5495  fssres  5503  f1co  5545  foun  5593  resdif  5596  f1oco  5597  fvun1  5702  elfvmptrab1  5731  fvreseq  5740  ftpg  5827  f1o2ndf1  6380  spc2ed  6385  smores  6444  nnaord  6663  nnm00  6684  brecop  6780  eroveu  6781  ecopovtrn  6787  ecopovtrng  6790  th3qlem1  6792  th3q  6795  ixpeq2  6867  djuexb  7222  addcmpblnq  7565  mulcmpblnq  7566  mulclnq  7574  dmaddpq  7577  dmmulpq  7578  mulcanenq  7583  distrnqg  7585  ltdcnq  7595  ltexnqq  7606  enq0breq  7634  mulcmpblnq0  7642  mulcanenq0ec  7643  addnnnq0  7647  mulnnnq0  7648  mulclnq0  7650  nqpnq0nq  7651  nqnq0a  7652  nqnq0m  7653  distrnq0  7657  elinp  7672  genpml  7715  genpmu  7716  genprndl  7719  genprndu  7720  addnqprl  7727  addnqpru  7728  distrlem1prl  7780  distrlem1pru  7781  ltsopr  7794  cauappcvgprlemdisj  7849  caucvgprlemdisj  7872  caucvgprprlemdisj  7900  addcmpblnr  7937  addsrpr  7943  mulsrpr  7944  addclsr  7951  addasssrg  7954  0idsr  7965  1idsr  7966  00sr  7967  mulgt0sr  7976  axaddcl  8062  axmulcl  8064  axaddass  8070  axdistr  8072  cnegexlem3  8334  cnegex  8335  apirr  8763  recexaplem2  8810  zletric  9501  zlelttric  9502  difgtsumgt  9527  qaddcl  9842  qmulcl  9844  qreccl  9849  iccss  10149  fzsubel  10268  elfz0add  10328  difelfznle  10343  2ffzeq  10349  fzonmapblen  10399  ubmelfzo  10418  ubmelm1fzo  10444  subfzo0  10460  qletric  10473  qlelttric  10474  adddivflid  10524  mulexp  10812  mulexpzap  10813  leexp1a  10828  faclbnd  10975  wrdeq  11106  ccatcl  11141  swrdsbslen  11214  swrdspsleq  11215  pfxccat1  11250  swrdswrdlem  11252  pfxccatin12lem2a  11275  swrdccatin2  11277  pfxccatin12lem2  11279  swrdccat  11283  reuccatpfxs1  11295  rexanuz  11515  sqabsadd  11582  sqabssub  11583  abs2dif  11633  rpmincl  11765  xrminrpcl  11801  fsum2dlemstep  11961  fprodeq0  12144  fprod2dlemstep  12149  summodnegmod  12349  dvds2ln  12351  dvdsflip  12378  gcdsupex  12494  gcdsupcl  12495  gcdabs  12525  sqgcd  12566  nnwosdc  12576  lcmabs  12614  lcmgcdlem  12615  lcmgcd  12616  lcmgcdeq  12621  qredeq  12634  cncongr1  12641  cncongr2  12642  hashgcdlem  12776  dvdsprmpweqle  12876  difsqpwdvds  12877  xpsfrnel2  13395  fngsum  13437  igsumvalx  13438  mndissubm  13524  resmhm2  13537  grpissubg  13747  subrngpropd  14196  subrgpropd  14233  tgcl  14754  uncld  14803  innei  14853  cnco  14911  txbas  14948  txbasval  14957  blin2  15122  qtopbasss  15211  lgsmulsqcoprm  15741  gausslemma2dlem1a  15753  lgsquad2lem2  15777  umgredgprv  15931  uspgredg2v  16035  usgredg2v  16038  wlkeq  16100  uspgr2wlkeq2  16112  uspgr2wlkeqi  16113  bj-charfunbi  16257  bj-indind  16378