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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  anim12ci  339  anim1i  340  anim2i  342  anifpdc  999  hban  1600  sbimi  1817  spsbbi  1897  2exeu  2179  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  sseq2  3272  unssin  3470  uneqin  3482  undif3ss  3492  prneimg  3899  ssunieq  3968  iuneq1  4025  iuneq2  4028  copsex2t  4385  soeq2  4461  tpexg  4590  eldifpw  4623  iunpw  4626  peano5  4745  opbrop  4854  xpsspw  4887  coeq1  4937  coeq2  4938  cnveq  4954  dmeq  4981  sotri  5183  elxp4  5275  elxp5  5276  funun  5422  fununfun  5424  fundif  5425  funtp  5434  imain  5463  2elresin  5494  funssxp  5557  fssres  5565  f1co  5610  foun  5658  resdif  5661  f1oco  5662  fvun1  5769  elfvmptrab1  5801  fvreseq  5812  ftpg  5899  f1o2ndf1  6464  spc2ed  6469  fvn0elsupp  6491  smores  6563  nnaord  6782  nnm00  6803  brecop  6899  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  th3q  6914  ixpeq2  6994  djuexb  7384  addcmpblnq  7734  mulcmpblnq  7735  mulclnq  7743  dmaddpq  7746  dmmulpq  7747  mulcanenq  7752  distrnqg  7754  ltdcnq  7764  ltexnqq  7775  enq0breq  7803  mulcmpblnq0  7811  mulcanenq0ec  7812  addnnnq0  7816  mulnnnq0  7817  mulclnq0  7819  nqpnq0nq  7820  nqnq0a  7821  nqnq0m  7822  distrnq0  7826  elinp  7841  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  addnqprl  7896  addnqpru  7897  distrlem1prl  7949  distrlem1pru  7950  ltsopr  7963  cauappcvgprlemdisj  8018  caucvgprlemdisj  8041  caucvgprprlemdisj  8069  addcmpblnr  8106  addsrpr  8112  mulsrpr  8113  addclsr  8120  addasssrg  8123  0idsr  8134  1idsr  8135  00sr  8136  mulgt0sr  8145  axaddcl  8231  axmulcl  8233  axaddass  8239  axdistr  8241  cnegexlem3  8503  cnegex  8504  apirr  8933  recexaplem2  8980  zletric  9688  zlelttric  9689  difgtsumgt  9714  qaddcl  10035  qmulcl  10037  qreccl  10042  iccss  10343  fzsubel  10466  elfz0add  10527  difelfznle  10542  2ffzeq  10548  fzonmapblen  10599  ubmelfzo  10618  ubmelm1fzo  10644  subfzo0  10661  qletric  10676  qlelttric  10677  adddivflid  10727  mulexp  11015  mulexpzap  11016  leexp1a  11031  faclbnd  11179  wrdeq  11326  ccatcl  11361  swrdsbslen  11438  swrdspsleq  11439  pfxccat1  11474  swrdswrdlem  11476  pfxccatin12lem2a  11499  swrdccatin2  11501  pfxccatin12lem2  11503  swrdccat  11507  reuccatpfxs1  11519  rexanuz  11754  sqabsadd  11821  sqabssub  11822  abs2dif  11872  rpmincl  12004  xrminrpcl  12040  fsum2dlemstep  12201  fprodeq0  12384  fprod2dlemstep  12389  summodnegmod  12589  dvds2ln  12591  dvdsflip  12618  gcdsupex  12734  gcdsupcl  12735  gcdabs  12765  sqgcd  12806  nnwosdc  12816  lcmabs  12854  lcmgcdlem  12855  lcmgcd  12856  lcmgcdeq  12861  qredeq  12874  cncongr1  12881  cncongr2  12882  hashgcdlem  13016  dvdsprmpweqle  13116  difsqpwdvds  13117  xpsfrnel2  13667  fngzsum  13708  gzsumvalx  13709  mndissubm  13782  resmhm2  13795  grpissubg  13997  subrngpropd  14524  subrgpropd  14561  tgcl  15165  uncld  15214  innei  15264  cnco  15322  txbas  15359  txbasval  15368  blin2  15533  qtopbasss  15622  lgsmulsqcoprm  16165  gausslemma2dlem1a  16177  lgsquad2lem2  16201  umgredgprv  16356  uspgredg2v  16462  usgredg2v  16465  wlkeq  16595  uspgr2wlkeq2  16607  uspgr2wlkeqi  16608  clwwlknonex2  16680  bj-charfunbi  16837  bj-indind  16958  als-no-surprise  17147  alseu-no-surprise  17179