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  4387  soeq2  4463  tpexg  4592  eldifpw  4625  iunpw  4628  peano5  4747  opbrop  4856  xpsspw  4889  coeq1  4939  coeq2  4940  cnveq  4956  dmeq  4983  sotri  5186  elxp4  5278  elxp5  5279  funun  5425  fununfun  5427  fundif  5428  funtp  5437  imain  5466  2elresin  5497  funssxp  5560  fssres  5568  f1co  5613  foun  5661  resdif  5664  f1oco  5665  fvun1  5772  elfvmptrab1  5804  fvreseq  5815  ftpg  5902  f1o2ndf1  6468  spc2ed  6473  fvn0elsupp  6495  smores  6567  nnaord  6786  nnm00  6807  brecop  6903  eroveu  6904  ecopovtrn  6910  ecopovtrng  6913  th3qlem1  6915  th3q  6918  ixpeq2  6998  djuexb  7390  addcmpblnq  7740  mulcmpblnq  7741  mulclnq  7749  dmaddpq  7752  dmmulpq  7753  mulcanenq  7758  distrnqg  7760  ltdcnq  7770  ltexnqq  7781  enq0breq  7809  mulcmpblnq0  7817  mulcanenq0ec  7818  addnnnq0  7822  mulnnnq0  7823  mulclnq0  7825  nqpnq0nq  7826  nqnq0a  7827  nqnq0m  7828  distrnq0  7832  elinp  7847  genpml  7890  genpmu  7891  genprndl  7894  genprndu  7895  addnqprl  7902  addnqpru  7903  distrlem1prl  7955  distrlem1pru  7956  ltsopr  7969  cauappcvgprlemdisj  8024  caucvgprlemdisj  8047  caucvgprprlemdisj  8075  addcmpblnr  8112  addsrpr  8118  mulsrpr  8119  addclsr  8126  addasssrg  8129  0idsr  8140  1idsr  8141  00sr  8142  mulgt0sr  8151  axaddcl  8237  axmulcl  8239  axaddass  8245  axdistr  8247  cnegexlem3  8510  cnegex  8511  apirr  8941  recexaplem2  8988  zletric  9699  zlelttric  9700  difgtsumgt  9725  qaddcl  10051  qmulcl  10053  qreccl  10058  iccss  10360  fzsubel  10483  elfz0add  10544  difelfznle  10559  2ffzeq  10565  fzonmapblen  10616  ubmelfzo  10635  ubmelm1fzo  10661  subfzo0  10678  qletric  10693  qlelttric  10694  adddivflid  10748  mulexp  11036  mulexpzap  11037  leexp1a  11052  faclbnd  11201  wrdeq  11348  ccatcl  11383  swrdsbslen  11460  swrdspsleq  11461  pfxccat1  11496  swrdswrdlem  11498  pfxccatin12lem2a  11521  swrdccatin2  11523  pfxccatin12lem2  11525  swrdccat  11529  reuccatpfxs1  11541  rexanuz  11776  sqabsadd  11843  sqabssub  11844  abs2dif  11895  rpmincl  12028  xrminrpcl  12065  fsum2dlemstep  12226  fprodeq0  12409  fprod2dlemstep  12414  summodnegmod  12614  dvds2ln  12616  dvdsflip  12643  gcdsupex  12759  gcdsupcl  12760  gcdabs  12790  sqgcd  12831  nnwosdc  12841  lcmabs  12879  lcmgcdlem  12880  lcmgcd  12881  lcmgcdeq  12886  qredeq  12899  cncongr1  12906  cncongr2  12907  hashgcdlem  13045  dvdsprmpweqle  13145  difsqpwdvds  13146  xpsfrnel2  13726  fngzsum  13767  gzsumvalx  13768  mndissubm  13841  resmhm2  13854  grpissubg  14056  subrngpropd  14633  subrgpropd  14670  tgcl  15290  uncld  15339  innei  15389  cnco  15447  txbas  15484  txbasval  15493  blin2  15658  qtopbasss  15747  lgsmulsqcoprm  16370  gausslemma2dlem1a  16382  lgsquad2lem2  16406  umgredgprv  16561  uspgredg2v  16667  usgredg2v  16670  wlkeq  16800  uspgr2wlkeq2  16812  uspgr2wlkeqi  16813  clwwlknonex2  16885  bj-charfunbi  17042  bj-indind  17163  als-no-surprise  17354  alseu-no-surprise  17386