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  2837  cgsex4g  2838  spc2egv  2894  spc2gv  2895  sseq2  3249  unssin  3444  uneqin  3456  undif3ss  3466  prneimg  3855  ssunieq  3924  iuneq1  3981  iuneq2  3984  copsex2t  4335  soeq2  4411  tpexg  4539  eldifpw  4572  iunpw  4575  peano5  4694  opbrop  4803  xpsspw  4836  coeq1  4885  coeq2  4886  cnveq  4902  dmeq  4929  sotri  5130  elxp4  5222  elxp5  5223  funun  5368  fununfun  5370  fundif  5371  funtp  5380  imain  5409  2elresin  5440  funssxp  5501  fssres  5509  f1co  5551  foun  5599  resdif  5602  f1oco  5603  fvun1  5708  elfvmptrab1  5737  fvreseq  5746  ftpg  5833  f1o2ndf1  6388  spc2ed  6393  smores  6453  nnaord  6672  nnm00  6693  brecop  6789  eroveu  6790  ecopovtrn  6796  ecopovtrng  6799  th3qlem1  6801  th3q  6804  ixpeq2  6876  djuexb  7234  addcmpblnq  7577  mulcmpblnq  7578  mulclnq  7586  dmaddpq  7589  dmmulpq  7590  mulcanenq  7595  distrnqg  7597  ltdcnq  7607  ltexnqq  7618  enq0breq  7646  mulcmpblnq0  7654  mulcanenq0ec  7655  addnnnq0  7659  mulnnnq0  7660  mulclnq0  7662  nqpnq0nq  7663  nqnq0a  7664  nqnq0m  7665  distrnq0  7669  elinp  7684  genpml  7727  genpmu  7728  genprndl  7731  genprndu  7732  addnqprl  7739  addnqpru  7740  distrlem1prl  7792  distrlem1pru  7793  ltsopr  7806  cauappcvgprlemdisj  7861  caucvgprlemdisj  7884  caucvgprprlemdisj  7912  addcmpblnr  7949  addsrpr  7955  mulsrpr  7956  addclsr  7963  addasssrg  7966  0idsr  7977  1idsr  7978  00sr  7979  mulgt0sr  7988  axaddcl  8074  axmulcl  8076  axaddass  8082  axdistr  8084  cnegexlem3  8346  cnegex  8347  apirr  8775  recexaplem2  8822  zletric  9513  zlelttric  9514  difgtsumgt  9539  qaddcl  9859  qmulcl  9861  qreccl  9866  iccss  10166  fzsubel  10285  elfz0add  10345  difelfznle  10360  2ffzeq  10366  fzonmapblen  10416  ubmelfzo  10435  ubmelm1fzo  10461  subfzo0  10478  qletric  10491  qlelttric  10492  adddivflid  10542  mulexp  10830  mulexpzap  10831  leexp1a  10846  faclbnd  10993  wrdeq  11125  ccatcl  11160  swrdsbslen  11237  swrdspsleq  11238  pfxccat1  11273  swrdswrdlem  11275  pfxccatin12lem2a  11298  swrdccatin2  11300  pfxccatin12lem2  11302  swrdccat  11306  reuccatpfxs1  11318  rexanuz  11539  sqabsadd  11606  sqabssub  11607  abs2dif  11657  rpmincl  11789  xrminrpcl  11825  fsum2dlemstep  11985  fprodeq0  12168  fprod2dlemstep  12173  summodnegmod  12373  dvds2ln  12375  dvdsflip  12402  gcdsupex  12518  gcdsupcl  12519  gcdabs  12549  sqgcd  12590  nnwosdc  12600  lcmabs  12638  lcmgcdlem  12639  lcmgcd  12640  lcmgcdeq  12645  qredeq  12658  cncongr1  12665  cncongr2  12666  hashgcdlem  12800  dvdsprmpweqle  12900  difsqpwdvds  12901  xpsfrnel2  13419  fngsum  13461  igsumvalx  13462  mndissubm  13548  resmhm2  13561  grpissubg  13771  subrngpropd  14220  subrgpropd  14257  tgcl  14778  uncld  14827  innei  14877  cnco  14935  txbas  14972  txbasval  14981  blin2  15146  qtopbasss  15235  lgsmulsqcoprm  15765  gausslemma2dlem1a  15777  lgsquad2lem2  15801  umgredgprv  15956  uspgredg2v  16060  usgredg2v  16063  wlkeq  16151  uspgr2wlkeq2  16163  uspgr2wlkeqi  16164  clwwlknonex2  16234  bj-charfunbi  16342  bj-indind  16463