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  2130  cgsex2g  2788  cgsex4g  2789  spc2egv  2842  spc2gv  2843  sseq2  3194  unssin  3389  uneqin  3401  undif3ss  3411  prneimg  3792  ssunieq  3860  iuneq1  3917  iuneq2  3920  copsex2t  4266  soeq2  4337  tpexg  4465  eldifpw  4498  iunpw  4501  peano5  4618  opbrop  4726  xpsspw  4759  coeq1  4805  coeq2  4806  cnveq  4822  dmeq  4848  sotri  5045  elxp4  5137  elxp5  5138  funun  5282  funtp  5291  imain  5320  2elresin  5349  funssxp  5407  fssres  5413  f1co  5455  foun  5502  resdif  5505  f1oco  5506  fvun1  5606  elfvmptrab1  5634  fvreseq  5643  ftpg  5724  f1o2ndf1  6257  spc2ed  6262  smores  6321  nnaord  6538  nnm00  6559  brecop  6655  eroveu  6656  ecopovtrn  6662  ecopovtrng  6665  th3qlem1  6667  th3q  6670  ixpeq2  6742  djuexb  7077  addcmpblnq  7401  mulcmpblnq  7402  mulclnq  7410  dmaddpq  7413  dmmulpq  7414  mulcanenq  7419  distrnqg  7421  ltdcnq  7431  ltexnqq  7442  enq0breq  7470  mulcmpblnq0  7478  mulcanenq0ec  7479  addnnnq0  7483  mulnnnq0  7484  mulclnq0  7486  nqpnq0nq  7487  nqnq0a  7488  nqnq0m  7489  distrnq0  7493  elinp  7508  genpml  7551  genpmu  7552  genprndl  7555  genprndu  7556  addnqprl  7563  addnqpru  7564  distrlem1prl  7616  distrlem1pru  7617  ltsopr  7630  cauappcvgprlemdisj  7685  caucvgprlemdisj  7708  caucvgprprlemdisj  7736  addcmpblnr  7773  addsrpr  7779  mulsrpr  7780  addclsr  7787  addasssrg  7790  0idsr  7801  1idsr  7802  00sr  7803  mulgt0sr  7812  axaddcl  7898  axmulcl  7900  axaddass  7906  axdistr  7908  cnegexlem3  8169  cnegex  8170  apirr  8597  recexaplem2  8644  zletric  9332  zlelttric  9333  difgtsumgt  9357  qaddcl  9671  qmulcl  9673  qreccl  9678  iccss  9977  fzsubel  10096  elfz0add  10156  difelfznle  10171  2ffzeq  10177  fzonmapblen  10223  ubmelfzo  10236  ubmelm1fzo  10262  subfzo0  10278  qletric  10280  qlelttric  10281  adddivflid  10329  mulexp  10599  mulexpzap  10600  leexp1a  10615  faclbnd  10762  rexanuz  11038  sqabsadd  11105  sqabssub  11106  abs2dif  11156  rpmincl  11287  xrminrpcl  11323  fsum2dlemstep  11483  fprodeq0  11666  fprod2dlemstep  11671  summodnegmod  11870  dvds2ln  11872  dvdsflip  11898  gcdsupex  11999  gcdsupcl  12000  gcdabs  12030  sqgcd  12071  nnwosdc  12081  lcmabs  12119  lcmgcdlem  12120  lcmgcd  12121  lcmgcdeq  12126  qredeq  12139  cncongr1  12146  cncongr2  12147  hashgcdlem  12281  dvdsprmpweqle  12380  difsqpwdvds  12381  xpsfrnel2  12833  fngsum  12875  igsumvalx  12876  mndissubm  12950  resmhm2  12963  grpissubg  13158  subrngpropd  13588  subrgpropd  13620  tgcl  14049  uncld  14098  innei  14148  cnco  14206  txbas  14243  txbasval  14252  blin2  14417  qtopbasss  14506  lgsmulsqcoprm  14933  bj-charfunbi  15049  bj-indind  15170