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  1558  sbimi  1775  spsbbi  1855  2exeu  2134  cgsex2g  2796  cgsex4g  2797  spc2egv  2851  spc2gv  2852  sseq2  3204  unssin  3399  uneqin  3411  undif3ss  3421  prneimg  3801  ssunieq  3869  iuneq1  3926  iuneq2  3929  copsex2t  4275  soeq2  4348  tpexg  4476  eldifpw  4509  iunpw  4512  peano5  4631  opbrop  4739  xpsspw  4772  coeq1  4820  coeq2  4821  cnveq  4837  dmeq  4863  sotri  5062  elxp4  5154  elxp5  5155  funun  5299  funtp  5308  imain  5337  2elresin  5366  funssxp  5424  fssres  5430  f1co  5472  foun  5520  resdif  5523  f1oco  5524  fvun1  5624  elfvmptrab1  5653  fvreseq  5662  ftpg  5743  f1o2ndf1  6283  spc2ed  6288  smores  6347  nnaord  6564  nnm00  6585  brecop  6681  eroveu  6682  ecopovtrn  6688  ecopovtrng  6691  th3qlem1  6693  th3q  6696  ixpeq2  6768  djuexb  7105  addcmpblnq  7429  mulcmpblnq  7430  mulclnq  7438  dmaddpq  7441  dmmulpq  7442  mulcanenq  7447  distrnqg  7449  ltdcnq  7459  ltexnqq  7470  enq0breq  7498  mulcmpblnq0  7506  mulcanenq0ec  7507  addnnnq0  7511  mulnnnq0  7512  mulclnq0  7514  nqpnq0nq  7515  nqnq0a  7516  nqnq0m  7517  distrnq0  7521  elinp  7536  genpml  7579  genpmu  7580  genprndl  7583  genprndu  7584  addnqprl  7591  addnqpru  7592  distrlem1prl  7644  distrlem1pru  7645  ltsopr  7658  cauappcvgprlemdisj  7713  caucvgprlemdisj  7736  caucvgprprlemdisj  7764  addcmpblnr  7801  addsrpr  7807  mulsrpr  7808  addclsr  7815  addasssrg  7818  0idsr  7829  1idsr  7830  00sr  7831  mulgt0sr  7840  axaddcl  7926  axmulcl  7928  axaddass  7934  axdistr  7936  cnegexlem3  8198  cnegex  8199  apirr  8626  recexaplem2  8673  zletric  9364  zlelttric  9365  difgtsumgt  9389  qaddcl  9703  qmulcl  9705  qreccl  9710  iccss  10010  fzsubel  10129  elfz0add  10189  difelfznle  10204  2ffzeq  10210  fzonmapblen  10257  ubmelfzo  10270  ubmelm1fzo  10296  subfzo0  10312  qletric  10314  qlelttric  10315  adddivflid  10364  mulexp  10652  mulexpzap  10653  leexp1a  10668  faclbnd  10815  wrdeq  10939  rexanuz  11135  sqabsadd  11202  sqabssub  11203  abs2dif  11253  rpmincl  11384  xrminrpcl  11420  fsum2dlemstep  11580  fprodeq0  11763  fprod2dlemstep  11768  summodnegmod  11968  dvds2ln  11970  dvdsflip  11996  gcdsupex  12097  gcdsupcl  12098  gcdabs  12128  sqgcd  12169  nnwosdc  12179  lcmabs  12217  lcmgcdlem  12218  lcmgcd  12219  lcmgcdeq  12224  qredeq  12237  cncongr1  12244  cncongr2  12245  hashgcdlem  12379  dvdsprmpweqle  12478  difsqpwdvds  12479  xpsfrnel2  12932  fngsum  12974  igsumvalx  12975  mndissubm  13050  resmhm2  13063  grpissubg  13267  subrngpropd  13715  subrgpropd  13752  tgcl  14243  uncld  14292  innei  14342  cnco  14400  txbas  14437  txbasval  14446  blin2  14611  qtopbasss  14700  lgsmulsqcoprm  15203  gausslemma2dlem1a  15215  lgsquad2lem2  15239  bj-charfunbi  15373  bj-indind  15494