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  anifpdc  992  hban  1593  sbimi  1810  spsbbi  1890  2exeu  2170  cgsex2g  2836  cgsex4g  2837  spc2egv  2893  spc2gv  2894  sseq2  3248  unssin  3443  uneqin  3455  undif3ss  3465  prneimg  3851  ssunieq  3920  iuneq1  3977  iuneq2  3980  copsex2t  4330  soeq2  4406  tpexg  4534  eldifpw  4567  iunpw  4570  peano5  4689  opbrop  4797  xpsspw  4830  coeq1  4878  coeq2  4879  cnveq  4895  dmeq  4922  sotri  5123  elxp4  5215  elxp5  5216  funun  5361  fununfun  5363  fundif  5364  funtp  5373  imain  5402  2elresin  5433  funssxp  5492  fssres  5500  f1co  5542  foun  5590  resdif  5593  f1oco  5594  fvun1  5699  elfvmptrab1  5728  fvreseq  5737  ftpg  5822  f1o2ndf1  6372  spc2ed  6377  smores  6436  nnaord  6653  nnm00  6674  brecop  6770  eroveu  6771  ecopovtrn  6777  ecopovtrng  6780  th3qlem1  6782  th3q  6785  ixpeq2  6857  djuexb  7207  addcmpblnq  7550  mulcmpblnq  7551  mulclnq  7559  dmaddpq  7562  dmmulpq  7563  mulcanenq  7568  distrnqg  7570  ltdcnq  7580  ltexnqq  7591  enq0breq  7619  mulcmpblnq0  7627  mulcanenq0ec  7628  addnnnq0  7632  mulnnnq0  7633  mulclnq0  7635  nqpnq0nq  7636  nqnq0a  7637  nqnq0m  7638  distrnq0  7642  elinp  7657  genpml  7700  genpmu  7701  genprndl  7704  genprndu  7705  addnqprl  7712  addnqpru  7713  distrlem1prl  7765  distrlem1pru  7766  ltsopr  7779  cauappcvgprlemdisj  7834  caucvgprlemdisj  7857  caucvgprprlemdisj  7885  addcmpblnr  7922  addsrpr  7928  mulsrpr  7929  addclsr  7936  addasssrg  7939  0idsr  7950  1idsr  7951  00sr  7952  mulgt0sr  7961  axaddcl  8047  axmulcl  8049  axaddass  8055  axdistr  8057  cnegexlem3  8319  cnegex  8320  apirr  8748  recexaplem2  8795  zletric  9486  zlelttric  9487  difgtsumgt  9512  qaddcl  9826  qmulcl  9828  qreccl  9833  iccss  10133  fzsubel  10252  elfz0add  10312  difelfznle  10327  2ffzeq  10333  fzonmapblen  10383  ubmelfzo  10401  ubmelm1fzo  10427  subfzo0  10443  qletric  10456  qlelttric  10457  adddivflid  10507  mulexp  10795  mulexpzap  10796  leexp1a  10811  faclbnd  10958  wrdeq  11088  ccatcl  11123  swrdsbslen  11193  swrdspsleq  11194  pfxccat1  11229  swrdswrdlem  11231  pfxccatin12lem2a  11254  swrdccatin2  11256  pfxccatin12lem2  11258  swrdccat  11262  reuccatpfxs1  11274  rexanuz  11494  sqabsadd  11561  sqabssub  11562  abs2dif  11612  rpmincl  11744  xrminrpcl  11780  fsum2dlemstep  11940  fprodeq0  12123  fprod2dlemstep  12128  summodnegmod  12328  dvds2ln  12330  dvdsflip  12357  gcdsupex  12473  gcdsupcl  12474  gcdabs  12504  sqgcd  12545  nnwosdc  12555  lcmabs  12593  lcmgcdlem  12594  lcmgcd  12595  lcmgcdeq  12600  qredeq  12613  cncongr1  12620  cncongr2  12621  hashgcdlem  12755  dvdsprmpweqle  12855  difsqpwdvds  12856  xpsfrnel2  13374  fngsum  13416  igsumvalx  13417  mndissubm  13503  resmhm2  13516  grpissubg  13726  subrngpropd  14174  subrgpropd  14211  tgcl  14732  uncld  14781  innei  14831  cnco  14889  txbas  14926  txbasval  14935  blin2  15100  qtopbasss  15189  lgsmulsqcoprm  15719  gausslemma2dlem1a  15731  lgsquad2lem2  15755  umgredgprv  15909  uspgredg2v  16013  usgredg2v  16016  bj-charfunbi  16132  bj-indind  16253