Theorem anim12i 331

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  anim12ci  332  anim1i  333  anim2i  334  hban  1484  sbimi  1694  spsbbi  1772  2exeu  2040  cgsex2g  2655  cgsex4g  2656  spc2egv  2708  spc2gv  2709  sseq2  3046  unssin  3236  uneqin  3248  undif3ss  3258  prneimg  3613  ssunieq  3681  iuneq1  3738  iuneq2  3741  copsex2t  4063  soeq2  4134  tpexg  4260  eldifpw  4289  iunpw  4292  peano5  4403  opbrop  4505  xpsspw  4538  coeq1  4581  coeq2  4582  cnveq  4598  dmeq  4624  sotri  4814  elxp4  4905  elxp5  4906  funun  5044  funtp  5053  imain  5082  2elresin  5111  funssxp  5165  fssres  5171  f1co  5212  foun  5256  resdif  5259  f1oco  5260  fvun1  5354  fvreseq  5387  ftpg  5465  f1o2ndf1  5975  spc2ed  5980  smores  6039  nnaord  6248  nnm00  6268  brecop  6362  eroveu  6363  ecopovtrn  6369  ecopovtrng  6372  th3qlem1  6374  th3q  6377  addcmpblnq  6905  mulcmpblnq  6906  mulclnq  6914  dmaddpq  6917  dmmulpq  6918  mulcanenq  6923  distrnqg  6925  ltdcnq  6935  ltexnqq  6946  enq0breq  6974  mulcmpblnq0  6982  mulcanenq0ec  6983  addnnnq0  6987  mulnnnq0  6988  mulclnq0  6990  nqpnq0nq  6991  nqnq0a  6992  nqnq0m  6993  distrnq0  6997  elinp  7012  genpml  7055  genpmu  7056  genprndl  7059  genprndu  7060  addnqprl  7067  addnqpru  7068  distrlem1prl  7120  distrlem1pru  7121  ltsopr  7134  cauappcvgprlemdisj  7189  caucvgprlemdisj  7212  caucvgprprlemdisj  7240  addcmpblnr  7264  addsrpr  7270  mulsrpr  7271  addclsr  7278  addasssrg  7281  0idsr  7292  1idsr  7293  00sr  7294  mulgt0sr  7302  axaddcl  7380  axmulcl  7382  axaddass  7386  axdistr  7388  cnegexlem3  7638  cnegex  7639  apirr  8058  recexaplem2  8095  zletric  8764  zlelttric  8765  qaddcl  9089  qmulcl  9091  qreccl  9096  iccss  9328  fzsubel  9442  elfz0add  9499  difelfznle  9511  2ffzeq  9517  fzonmapblen  9563  ubmelfzo  9576  ubmelm1fzo  9602  subfzo0  9618  qletric  9620  qlelttric  9621  adddivflid  9664  mulexp  9959  mulexpzap  9960  leexp1a  9975  faclbnd  10114  rexanuz  10386  sqabsadd  10453  sqabssub  10454  abs2dif  10504  fsum2dlemstep  10791  summodnegmod  10920  dvds2ln  10922  dvdsflip  10945  gcdsupex  11042  gcdsupcl  11043  gcdabs  11072  sqgcd  11111  lcmabs  11151  lcmgcdlem  11152  lcmgcd  11153  lcmgcdeq  11158  qredeq  11171  cncongr1  11178  cncongr2  11179  hashgcdlem  11296  bj-indind  11484