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  6568  nnaord  6787  nnm00  6808  brecop  6904  eroveu  6905  ecopovtrn  6911  ecopovtrng  6914  th3qlem1  6916  th3q  6919  ixpeq2  7000  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  9697  zlelttric  9698  difgtsumgt  9723  qaddcl  10050  qmulcl  10052  qreccl  10057  iccss  10359  fzsubel  10482  elfz0add  10543  difelfznle  10558  2ffzeq  10564  fzonmapblen  10615  ubmelfzo  10634  ubmelm1fzo  10660  subfzo0  10677  qletric  10692  qlelttric  10693  adddivflid  10747  mulexp  11035  mulexpzap  11036  leexp1a  11051  faclbnd  11200  wrdeq  11347  ccatcl  11382  swrdsbslen  11459  swrdspsleq  11460  pfxccat1  11495  swrdswrdlem  11497  pfxccatin12lem2a  11520  swrdccatin2  11522  pfxccatin12lem2  11524  swrdccat  11528  reuccatpfxs1  11540  rexanuz  11775  sqabsadd  11842  sqabssub  11843  abs2dif  11894  rpmincl  12027  xrminrpcl  12064  fsum2dlemstep  12225  fprodeq0  12408  fprod2dlemstep  12413  summodnegmod  12613  dvds2ln  12615  dvdsflip  12642  gcdsupex  12758  gcdsupcl  12759  gcdabs  12789  sqgcd  12830  nnwosdc  12840  lcmabs  12878  lcmgcdlem  12879  lcmgcd  12880  lcmgcdeq  12885  qredeq  12898  cncongr1  12905  cncongr2  12906  hashgcdlem  13044  dvdsprmpweqle  13144  difsqpwdvds  13145  xpsfrnel2  13725  fngzsum  13766  gzsumvalx  13767  mndissubm  13840  resmhm2  13853  grpissubg  14055  subrngpropd  14632  subrgpropd  14669  tgcl  15307  uncld  15356  innei  15406  cnco  15464  txbas  15501  txbasval  15510  blin2  15675  qtopbasss  15764  lgsmulsqcoprm  16387  gausslemma2dlem1a  16399  lgsquad2lem2  16423  umgredgprv  16578  uspgredg2v  16684  usgredg2v  16687  wlkeq  16817  uspgr2wlkeq2  16829  uspgr2wlkeqi  16830  clwwlknonex2  16902  bj-charfunbi  17059  bj-indind  17180  als-no-surprise  17371  alseu-no-surprise  17403