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  7385  addcmpblnq  7735  mulcmpblnq  7736  mulclnq  7744  dmaddpq  7747  dmmulpq  7748  mulcanenq  7753  distrnqg  7755  ltdcnq  7765  ltexnqq  7776  enq0breq  7804  mulcmpblnq0  7812  mulcanenq0ec  7813  addnnnq0  7817  mulnnnq0  7818  mulclnq0  7820  nqpnq0nq  7821  nqnq0a  7822  nqnq0m  7823  distrnq0  7827  elinp  7842  genpml  7885  genpmu  7886  genprndl  7889  genprndu  7890  addnqprl  7897  addnqpru  7898  distrlem1prl  7950  distrlem1pru  7951  ltsopr  7964  cauappcvgprlemdisj  8019  caucvgprlemdisj  8042  caucvgprprlemdisj  8070  addcmpblnr  8107  addsrpr  8113  mulsrpr  8114  addclsr  8121  addasssrg  8124  0idsr  8135  1idsr  8136  00sr  8137  mulgt0sr  8146  axaddcl  8232  axmulcl  8234  axaddass  8240  axdistr  8242  cnegexlem3  8505  cnegex  8506  apirr  8936  recexaplem2  8983  zletric  9693  zlelttric  9694  difgtsumgt  9719  qaddcl  10045  qmulcl  10047  qreccl  10052  iccss  10354  fzsubel  10477  elfz0add  10538  difelfznle  10553  2ffzeq  10559  fzonmapblen  10610  ubmelfzo  10629  ubmelm1fzo  10655  subfzo0  10672  qletric  10687  qlelttric  10688  adddivflid  10742  mulexp  11030  mulexpzap  11031  leexp1a  11046  faclbnd  11195  wrdeq  11342  ccatcl  11377  swrdsbslen  11454  swrdspsleq  11455  pfxccat1  11490  swrdswrdlem  11492  pfxccatin12lem2a  11515  swrdccatin2  11517  pfxccatin12lem2  11519  swrdccat  11523  reuccatpfxs1  11535  rexanuz  11770  sqabsadd  11837  sqabssub  11838  abs2dif  11889  rpmincl  12022  xrminrpcl  12059  fsum2dlemstep  12220  fprodeq0  12403  fprod2dlemstep  12408  summodnegmod  12608  dvds2ln  12610  dvdsflip  12637  gcdsupex  12753  gcdsupcl  12754  gcdabs  12784  sqgcd  12825  nnwosdc  12835  lcmabs  12873  lcmgcdlem  12874  lcmgcd  12875  lcmgcdeq  12880  qredeq  12893  cncongr1  12900  cncongr2  12901  hashgcdlem  13039  dvdsprmpweqle  13139  difsqpwdvds  13140  xpsfrnel2  13720  fngzsum  13761  gzsumvalx  13762  mndissubm  13835  resmhm2  13848  grpissubg  14050  subrngpropd  14608  subrgpropd  14645  tgcl  15256  uncld  15305  innei  15355  cnco  15413  txbas  15450  txbasval  15459  blin2  15624  qtopbasss  15713  lgsmulsqcoprm  16331  gausslemma2dlem1a  16343  lgsquad2lem2  16367  umgredgprv  16522  uspgredg2v  16628  usgredg2v  16631  wlkeq  16761  uspgr2wlkeq2  16773  uspgr2wlkeqi  16774  clwwlknonex2  16846  bj-charfunbi  17003  bj-indind  17124  als-no-surprise  17314  alseu-no-surprise  17346