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  8504  cnegex  8505  apirr  8935  recexaplem2  8982  zletric  9692  zlelttric  9693  difgtsumgt  9718  qaddcl  10044  qmulcl  10046  qreccl  10051  iccss  10353  fzsubel  10476  elfz0add  10537  difelfznle  10552  2ffzeq  10558  fzonmapblen  10609  ubmelfzo  10628  ubmelm1fzo  10654  subfzo0  10671  qletric  10686  qlelttric  10687  adddivflid  10740  mulexp  11028  mulexpzap  11029  leexp1a  11044  faclbnd  11193  wrdeq  11340  ccatcl  11375  swrdsbslen  11452  swrdspsleq  11453  pfxccat1  11488  swrdswrdlem  11490  pfxccatin12lem2a  11513  swrdccatin2  11515  pfxccatin12lem2  11517  swrdccat  11521  reuccatpfxs1  11533  rexanuz  11768  sqabsadd  11835  sqabssub  11836  abs2dif  11887  rpmincl  12019  xrminrpcl  12056  fsum2dlemstep  12217  fprodeq0  12400  fprod2dlemstep  12405  summodnegmod  12605  dvds2ln  12607  dvdsflip  12634  gcdsupex  12750  gcdsupcl  12751  gcdabs  12781  sqgcd  12822  nnwosdc  12832  lcmabs  12870  lcmgcdlem  12871  lcmgcd  12872  lcmgcdeq  12877  qredeq  12890  cncongr1  12897  cncongr2  12898  hashgcdlem  13036  dvdsprmpweqle  13136  difsqpwdvds  13137  xpsfrnel2  13716  fngzsum  13757  gzsumvalx  13758  mndissubm  13831  resmhm2  13844  grpissubg  14046  subrngpropd  14573  subrgpropd  14610  tgcl  15214  uncld  15263  innei  15313  cnco  15371  txbas  15408  txbasval  15417  blin2  15582  qtopbasss  15671  lgsmulsqcoprm  16263  gausslemma2dlem1a  16275  lgsquad2lem2  16299  umgredgprv  16454  uspgredg2v  16560  usgredg2v  16563  wlkeq  16693  uspgr2wlkeq2  16705  uspgr2wlkeqi  16706  clwwlknonex2  16778  bj-charfunbi  16935  bj-indind  17056  als-no-surprise  17245  alseu-no-surprise  17277