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  1561  sbimi  1778  spsbbi  1858  2exeu  2137  cgsex2g  2799  cgsex4g  2800  spc2egv  2854  spc2gv  2855  sseq2  3208  unssin  3403  uneqin  3415  undif3ss  3425  prneimg  3805  ssunieq  3873  iuneq1  3930  iuneq2  3933  copsex2t  4279  soeq2  4352  tpexg  4480  eldifpw  4513  iunpw  4516  peano5  4635  opbrop  4743  xpsspw  4776  coeq1  4824  coeq2  4825  cnveq  4841  dmeq  4867  sotri  5066  elxp4  5158  elxp5  5159  funun  5303  funtp  5312  imain  5341  2elresin  5372  funssxp  5430  fssres  5436  f1co  5478  foun  5526  resdif  5529  f1oco  5530  fvun1  5630  elfvmptrab1  5659  fvreseq  5668  ftpg  5749  f1o2ndf1  6295  spc2ed  6300  smores  6359  nnaord  6576  nnm00  6597  brecop  6693  eroveu  6694  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  th3q  6708  ixpeq2  6780  djuexb  7119  addcmpblnq  7453  mulcmpblnq  7454  mulclnq  7462  dmaddpq  7465  dmmulpq  7466  mulcanenq  7471  distrnqg  7473  ltdcnq  7483  ltexnqq  7494  enq0breq  7522  mulcmpblnq0  7530  mulcanenq0ec  7531  addnnnq0  7535  mulnnnq0  7536  mulclnq0  7538  nqpnq0nq  7539  nqnq0a  7540  nqnq0m  7541  distrnq0  7545  elinp  7560  genpml  7603  genpmu  7604  genprndl  7607  genprndu  7608  addnqprl  7615  addnqpru  7616  distrlem1prl  7668  distrlem1pru  7669  ltsopr  7682  cauappcvgprlemdisj  7737  caucvgprlemdisj  7760  caucvgprprlemdisj  7788  addcmpblnr  7825  addsrpr  7831  mulsrpr  7832  addclsr  7839  addasssrg  7842  0idsr  7853  1idsr  7854  00sr  7855  mulgt0sr  7864  axaddcl  7950  axmulcl  7952  axaddass  7958  axdistr  7960  cnegexlem3  8222  cnegex  8223  apirr  8651  recexaplem2  8698  zletric  9389  zlelttric  9390  difgtsumgt  9414  qaddcl  9728  qmulcl  9730  qreccl  9735  iccss  10035  fzsubel  10154  elfz0add  10214  difelfznle  10229  2ffzeq  10235  fzonmapblen  10282  ubmelfzo  10295  ubmelm1fzo  10321  subfzo0  10337  qletric  10350  qlelttric  10351  adddivflid  10401  mulexp  10689  mulexpzap  10690  leexp1a  10705  faclbnd  10852  wrdeq  10976  rexanuz  11172  sqabsadd  11239  sqabssub  11240  abs2dif  11290  rpmincl  11422  xrminrpcl  11458  fsum2dlemstep  11618  fprodeq0  11801  fprod2dlemstep  11806  summodnegmod  12006  dvds2ln  12008  dvdsflip  12035  gcdsupex  12151  gcdsupcl  12152  gcdabs  12182  sqgcd  12223  nnwosdc  12233  lcmabs  12271  lcmgcdlem  12272  lcmgcd  12273  lcmgcdeq  12278  qredeq  12291  cncongr1  12298  cncongr2  12299  hashgcdlem  12433  dvdsprmpweqle  12533  difsqpwdvds  12534  xpsfrnel2  13050  fngsum  13092  igsumvalx  13093  mndissubm  13179  resmhm2  13192  grpissubg  13402  subrngpropd  13850  subrgpropd  13887  tgcl  14408  uncld  14457  innei  14507  cnco  14565  txbas  14602  txbasval  14611  blin2  14776  qtopbasss  14865  lgsmulsqcoprm  15395  gausslemma2dlem1a  15407  lgsquad2lem2  15431  bj-charfunbi  15565  bj-indind  15686