Theorem anim12i 336

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 287	1 |- ( ( ph /\ ch ) -> ( ps /\ th ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  anim12ci  337  anim1i  338  anim2i  340  hban  1535  sbimi  1752  spsbbi  1832  2exeu  2106  cgsex2g  2762  cgsex4g  2763  spc2egv  2816  spc2gv  2817  sseq2  3166  unssin  3361  uneqin  3373  undif3ss  3383  prneimg  3754  ssunieq  3822  iuneq1  3879  iuneq2  3882  copsex2t  4223  soeq2  4294  tpexg  4422  eldifpw  4455  iunpw  4458  peano5  4575  opbrop  4683  xpsspw  4716  coeq1  4761  coeq2  4762  cnveq  4778  dmeq  4804  sotri  4999  elxp4  5091  elxp5  5092  funun  5232  funtp  5241  imain  5270  2elresin  5299  funssxp  5357  fssres  5363  f1co  5405  foun  5451  resdif  5454  f1oco  5455  fvun1  5552  elfvmptrab1  5580  fvreseq  5589  ftpg  5669  f1o2ndf1  6196  spc2ed  6201  smores  6260  nnaord  6477  nnm00  6497  brecop  6591  eroveu  6592  ecopovtrn  6598  ecopovtrng  6601  th3qlem1  6603  th3q  6606  ixpeq2  6678  djuexb  7009  addcmpblnq  7308  mulcmpblnq  7309  mulclnq  7317  dmaddpq  7320  dmmulpq  7321  mulcanenq  7326  distrnqg  7328  ltdcnq  7338  ltexnqq  7349  enq0breq  7377  mulcmpblnq0  7385  mulcanenq0ec  7386  addnnnq0  7390  mulnnnq0  7391  mulclnq0  7393  nqpnq0nq  7394  nqnq0a  7395  nqnq0m  7396  distrnq0  7400  elinp  7415  genpml  7458  genpmu  7459  genprndl  7462  genprndu  7463  addnqprl  7470  addnqpru  7471  distrlem1prl  7523  distrlem1pru  7524  ltsopr  7537  cauappcvgprlemdisj  7592  caucvgprlemdisj  7615  caucvgprprlemdisj  7643  addcmpblnr  7680  addsrpr  7686  mulsrpr  7687  addclsr  7694  addasssrg  7697  0idsr  7708  1idsr  7709  00sr  7710  mulgt0sr  7719  axaddcl  7805  axmulcl  7807  axaddass  7813  axdistr  7815  cnegexlem3  8075  cnegex  8076  apirr  8503  recexaplem2  8549  zletric  9235  zlelttric  9236  difgtsumgt  9260  qaddcl  9573  qmulcl  9575  qreccl  9580  iccss  9877  fzsubel  9995  elfz0add  10055  difelfznle  10070  2ffzeq  10076  fzonmapblen  10122  ubmelfzo  10135  ubmelm1fzo  10161  subfzo0  10177  qletric  10179  qlelttric  10180  adddivflid  10227  mulexp  10494  mulexpzap  10495  leexp1a  10510  faclbnd  10654  rexanuz  10930  sqabsadd  10997  sqabssub  10998  abs2dif  11048  rpmincl  11179  xrminrpcl  11215  fsum2dlemstep  11375  fprodeq0  11558  fprod2dlemstep  11563  summodnegmod  11762  dvds2ln  11764  dvdsflip  11789  gcdsupex  11890  gcdsupcl  11891  gcdabs  11921  sqgcd  11962  nnwosdc  11972  lcmabs  12008  lcmgcdlem  12009  lcmgcd  12010  lcmgcdeq  12015  qredeq  12028  cncongr1  12035  cncongr2  12036  hashgcdlem  12170  dvdsprmpweqle  12268  difsqpwdvds  12269  tgcl  12704  uncld  12753  innei  12803  cnco  12861  txbas  12898  txbasval  12907  blin2  13072  qtopbasss  13161  lgsmulsqcoprm  13587  bj-charfunbi  13693  bj-indind  13814