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  hban  1547  sbimi  1764  spsbbi  1844  2exeu  2118  cgsex2g  2775  cgsex4g  2776  spc2egv  2829  spc2gv  2830  sseq2  3181  unssin  3376  uneqin  3388  undif3ss  3398  prneimg  3776  ssunieq  3844  iuneq1  3901  iuneq2  3904  copsex2t  4247  soeq2  4318  tpexg  4446  eldifpw  4479  iunpw  4482  peano5  4599  opbrop  4707  xpsspw  4740  coeq1  4786  coeq2  4787  cnveq  4803  dmeq  4829  sotri  5026  elxp4  5118  elxp5  5119  funun  5262  funtp  5271  imain  5300  2elresin  5329  funssxp  5387  fssres  5393  f1co  5435  foun  5482  resdif  5485  f1oco  5486  fvun1  5584  elfvmptrab1  5612  fvreseq  5621  ftpg  5702  f1o2ndf1  6231  spc2ed  6236  smores  6295  nnaord  6512  nnm00  6533  brecop  6627  eroveu  6628  ecopovtrn  6634  ecopovtrng  6637  th3qlem1  6639  th3q  6642  ixpeq2  6714  djuexb  7045  addcmpblnq  7368  mulcmpblnq  7369  mulclnq  7377  dmaddpq  7380  dmmulpq  7381  mulcanenq  7386  distrnqg  7388  ltdcnq  7398  ltexnqq  7409  enq0breq  7437  mulcmpblnq0  7445  mulcanenq0ec  7446  addnnnq0  7450  mulnnnq0  7451  mulclnq0  7453  nqpnq0nq  7454  nqnq0a  7455  nqnq0m  7456  distrnq0  7460  elinp  7475  genpml  7518  genpmu  7519  genprndl  7522  genprndu  7523  addnqprl  7530  addnqpru  7531  distrlem1prl  7583  distrlem1pru  7584  ltsopr  7597  cauappcvgprlemdisj  7652  caucvgprlemdisj  7675  caucvgprprlemdisj  7703  addcmpblnr  7740  addsrpr  7746  mulsrpr  7747  addclsr  7754  addasssrg  7757  0idsr  7768  1idsr  7769  00sr  7770  mulgt0sr  7779  axaddcl  7865  axmulcl  7867  axaddass  7873  axdistr  7875  cnegexlem3  8136  cnegex  8137  apirr  8564  recexaplem2  8611  zletric  9299  zlelttric  9300  difgtsumgt  9324  qaddcl  9637  qmulcl  9639  qreccl  9644  iccss  9943  fzsubel  10062  elfz0add  10122  difelfznle  10137  2ffzeq  10143  fzonmapblen  10189  ubmelfzo  10202  ubmelm1fzo  10228  subfzo0  10244  qletric  10246  qlelttric  10247  adddivflid  10294  mulexp  10561  mulexpzap  10562  leexp1a  10577  faclbnd  10723  rexanuz  10999  sqabsadd  11066  sqabssub  11067  abs2dif  11117  rpmincl  11248  xrminrpcl  11284  fsum2dlemstep  11444  fprodeq0  11627  fprod2dlemstep  11632  summodnegmod  11831  dvds2ln  11833  dvdsflip  11859  gcdsupex  11960  gcdsupcl  11961  gcdabs  11991  sqgcd  12032  nnwosdc  12042  lcmabs  12078  lcmgcdlem  12079  lcmgcd  12080  lcmgcdeq  12085  qredeq  12098  cncongr1  12105  cncongr2  12106  hashgcdlem  12240  dvdsprmpweqle  12338  difsqpwdvds  12339  xpsfrnel2  12770  mndissubm  12871  grpissubg  13059  subrgpropd  13374  tgcl  13649  uncld  13698  innei  13748  cnco  13806  txbas  13843  txbasval  13852  blin2  14017  qtopbasss  14106  lgsmulsqcoprm  14532  bj-charfunbi  14648  bj-indind  14769