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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  anim12ci  339  anim1i  340  anim2i  342  hban  1571  sbimi  1788  spsbbi  1868  2exeu  2148  cgsex2g  2813  cgsex4g  2814  spc2egv  2870  spc2gv  2871  sseq2  3225  unssin  3420  uneqin  3432  undif3ss  3442  prneimg  3828  ssunieq  3897  iuneq1  3954  iuneq2  3957  copsex2t  4307  soeq2  4381  tpexg  4509  eldifpw  4542  iunpw  4545  peano5  4664  opbrop  4772  xpsspw  4805  coeq1  4853  coeq2  4854  cnveq  4870  dmeq  4897  sotri  5097  elxp4  5189  elxp5  5190  funun  5334  fununfun  5336  fundif  5337  funtp  5346  imain  5375  2elresin  5406  funssxp  5465  fssres  5473  f1co  5515  foun  5563  resdif  5566  f1oco  5567  fvun1  5668  elfvmptrab1  5697  fvreseq  5706  ftpg  5791  f1o2ndf1  6337  spc2ed  6342  smores  6401  nnaord  6618  nnm00  6639  brecop  6735  eroveu  6736  ecopovtrn  6742  ecopovtrng  6745  th3qlem1  6747  th3q  6750  ixpeq2  6822  djuexb  7172  addcmpblnq  7515  mulcmpblnq  7516  mulclnq  7524  dmaddpq  7527  dmmulpq  7528  mulcanenq  7533  distrnqg  7535  ltdcnq  7545  ltexnqq  7556  enq0breq  7584  mulcmpblnq0  7592  mulcanenq0ec  7593  addnnnq0  7597  mulnnnq0  7598  mulclnq0  7600  nqpnq0nq  7601  nqnq0a  7602  nqnq0m  7603  distrnq0  7607  elinp  7622  genpml  7665  genpmu  7666  genprndl  7669  genprndu  7670  addnqprl  7677  addnqpru  7678  distrlem1prl  7730  distrlem1pru  7731  ltsopr  7744  cauappcvgprlemdisj  7799  caucvgprlemdisj  7822  caucvgprprlemdisj  7850  addcmpblnr  7887  addsrpr  7893  mulsrpr  7894  addclsr  7901  addasssrg  7904  0idsr  7915  1idsr  7916  00sr  7917  mulgt0sr  7926  axaddcl  8012  axmulcl  8014  axaddass  8020  axdistr  8022  cnegexlem3  8284  cnegex  8285  apirr  8713  recexaplem2  8760  zletric  9451  zlelttric  9452  difgtsumgt  9477  qaddcl  9791  qmulcl  9793  qreccl  9798  iccss  10098  fzsubel  10217  elfz0add  10277  difelfznle  10292  2ffzeq  10298  fzonmapblen  10348  ubmelfzo  10366  ubmelm1fzo  10392  subfzo0  10408  qletric  10421  qlelttric  10422  adddivflid  10472  mulexp  10760  mulexpzap  10761  leexp1a  10776  faclbnd  10923  wrdeq  11053  ccatcl  11087  swrdsbslen  11157  swrdspsleq  11158  pfxccat1  11193  swrdswrdlem  11195  pfxccatin12lem2a  11218  swrdccatin2  11220  pfxccatin12lem2  11222  swrdccat  11226  reuccatpfxs1  11238  rexanuz  11414  sqabsadd  11481  sqabssub  11482  abs2dif  11532  rpmincl  11664  xrminrpcl  11700  fsum2dlemstep  11860  fprodeq0  12043  fprod2dlemstep  12048  summodnegmod  12248  dvds2ln  12250  dvdsflip  12277  gcdsupex  12393  gcdsupcl  12394  gcdabs  12424  sqgcd  12465  nnwosdc  12475  lcmabs  12513  lcmgcdlem  12514  lcmgcd  12515  lcmgcdeq  12520  qredeq  12533  cncongr1  12540  cncongr2  12541  hashgcdlem  12675  dvdsprmpweqle  12775  difsqpwdvds  12776  xpsfrnel2  13293  fngsum  13335  igsumvalx  13336  mndissubm  13422  resmhm2  13435  grpissubg  13645  subrngpropd  14093  subrgpropd  14130  tgcl  14651  uncld  14700  innei  14750  cnco  14808  txbas  14845  txbasval  14854  blin2  15019  qtopbasss  15108  lgsmulsqcoprm  15638  gausslemma2dlem1a  15650  lgsquad2lem2  15674  bj-charfunbi  15946  bj-indind  16067