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  1570  sbimi  1787  spsbbi  1867  2exeu  2146  cgsex2g  2808  cgsex4g  2809  spc2egv  2863  spc2gv  2864  sseq2  3217  unssin  3412  uneqin  3424  undif3ss  3434  prneimg  3815  ssunieq  3883  iuneq1  3940  iuneq2  3943  copsex2t  4289  soeq2  4363  tpexg  4491  eldifpw  4524  iunpw  4527  peano5  4646  opbrop  4754  xpsspw  4787  coeq1  4835  coeq2  4836  cnveq  4852  dmeq  4878  sotri  5078  elxp4  5170  elxp5  5171  funun  5315  fununfun  5317  fundif  5318  funtp  5327  imain  5356  2elresin  5387  funssxp  5445  fssres  5451  f1co  5493  foun  5541  resdif  5544  f1oco  5545  fvun1  5645  elfvmptrab1  5674  fvreseq  5683  ftpg  5768  f1o2ndf1  6314  spc2ed  6319  smores  6378  nnaord  6595  nnm00  6616  brecop  6712  eroveu  6713  ecopovtrn  6719  ecopovtrng  6722  th3qlem1  6724  th3q  6727  ixpeq2  6799  djuexb  7146  addcmpblnq  7480  mulcmpblnq  7481  mulclnq  7489  dmaddpq  7492  dmmulpq  7493  mulcanenq  7498  distrnqg  7500  ltdcnq  7510  ltexnqq  7521  enq0breq  7549  mulcmpblnq0  7557  mulcanenq0ec  7558  addnnnq0  7562  mulnnnq0  7563  mulclnq0  7565  nqpnq0nq  7566  nqnq0a  7567  nqnq0m  7568  distrnq0  7572  elinp  7587  genpml  7630  genpmu  7631  genprndl  7634  genprndu  7635  addnqprl  7642  addnqpru  7643  distrlem1prl  7695  distrlem1pru  7696  ltsopr  7709  cauappcvgprlemdisj  7764  caucvgprlemdisj  7787  caucvgprprlemdisj  7815  addcmpblnr  7852  addsrpr  7858  mulsrpr  7859  addclsr  7866  addasssrg  7869  0idsr  7880  1idsr  7881  00sr  7882  mulgt0sr  7891  axaddcl  7977  axmulcl  7979  axaddass  7985  axdistr  7987  cnegexlem3  8249  cnegex  8250  apirr  8678  recexaplem2  8725  zletric  9416  zlelttric  9417  difgtsumgt  9442  qaddcl  9756  qmulcl  9758  qreccl  9763  iccss  10063  fzsubel  10182  elfz0add  10242  difelfznle  10257  2ffzeq  10263  fzonmapblen  10311  ubmelfzo  10329  ubmelm1fzo  10355  subfzo0  10371  qletric  10384  qlelttric  10385  adddivflid  10435  mulexp  10723  mulexpzap  10724  leexp1a  10739  faclbnd  10886  wrdeq  11016  ccatcl  11049  swrdsbslen  11119  swrdspsleq  11120  rexanuz  11299  sqabsadd  11366  sqabssub  11367  abs2dif  11417  rpmincl  11549  xrminrpcl  11585  fsum2dlemstep  11745  fprodeq0  11928  fprod2dlemstep  11933  summodnegmod  12133  dvds2ln  12135  dvdsflip  12162  gcdsupex  12278  gcdsupcl  12279  gcdabs  12309  sqgcd  12350  nnwosdc  12360  lcmabs  12398  lcmgcdlem  12399  lcmgcd  12400  lcmgcdeq  12405  qredeq  12418  cncongr1  12425  cncongr2  12426  hashgcdlem  12560  dvdsprmpweqle  12660  difsqpwdvds  12661  xpsfrnel2  13178  fngsum  13220  igsumvalx  13221  mndissubm  13307  resmhm2  13320  grpissubg  13530  subrngpropd  13978  subrgpropd  14015  tgcl  14536  uncld  14585  innei  14635  cnco  14693  txbas  14730  txbasval  14739  blin2  14904  qtopbasss  14993  lgsmulsqcoprm  15523  gausslemma2dlem1a  15535  lgsquad2lem2  15559  bj-charfunbi  15747  bj-indind  15868