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  anifpdc  995  hban  1596  sbimi  1813  spsbbi  1893  2exeu  2173  cgsex2g  2850  cgsex4g  2851  spc2egv  2907  spc2gv  2908  sseq2  3262  unssin  3460  uneqin  3472  undif3ss  3482  prneimg  3878  ssunieq  3947  iuneq1  4004  iuneq2  4007  copsex2t  4361  soeq2  4437  tpexg  4565  eldifpw  4598  iunpw  4601  peano5  4720  opbrop  4829  xpsspw  4862  coeq1  4912  coeq2  4913  cnveq  4929  dmeq  4956  sotri  5158  elxp4  5250  elxp5  5251  funun  5397  fununfun  5399  fundif  5400  funtp  5409  imain  5438  2elresin  5469  funssxp  5532  fssres  5540  f1co  5585  foun  5633  resdif  5636  f1oco  5637  fvun1  5743  elfvmptrab1  5772  fvreseq  5781  ftpg  5868  f1o2ndf1  6424  spc2ed  6429  fvn0elsupp  6451  smores  6523  nnaord  6742  nnm00  6763  brecop  6859  eroveu  6860  ecopovtrn  6866  ecopovtrng  6869  th3qlem1  6871  th3q  6874  ixpeq2  6947  djuexb  7335  addcmpblnq  7682  mulcmpblnq  7683  mulclnq  7691  dmaddpq  7694  dmmulpq  7695  mulcanenq  7700  distrnqg  7702  ltdcnq  7712  ltexnqq  7723  enq0breq  7751  mulcmpblnq0  7759  mulcanenq0ec  7760  addnnnq0  7764  mulnnnq0  7765  mulclnq0  7767  nqpnq0nq  7768  nqnq0a  7769  nqnq0m  7770  distrnq0  7774  elinp  7789  genpml  7832  genpmu  7833  genprndl  7836  genprndu  7837  addnqprl  7844  addnqpru  7845  distrlem1prl  7897  distrlem1pru  7898  ltsopr  7911  cauappcvgprlemdisj  7966  caucvgprlemdisj  7989  caucvgprprlemdisj  8017  addcmpblnr  8054  addsrpr  8060  mulsrpr  8061  addclsr  8068  addasssrg  8071  0idsr  8082  1idsr  8083  00sr  8084  mulgt0sr  8093  axaddcl  8179  axmulcl  8181  axaddass  8187  axdistr  8189  cnegexlem3  8450  cnegex  8451  apirr  8879  recexaplem2  8926  zletric  9621  zlelttric  9622  difgtsumgt  9647  qaddcl  9967  qmulcl  9969  qreccl  9974  iccss  10274  fzsubel  10394  elfz0add  10454  difelfznle  10469  2ffzeq  10475  fzonmapblen  10526  ubmelfzo  10545  ubmelm1fzo  10571  subfzo0  10588  qletric  10601  qlelttric  10602  adddivflid  10652  mulexp  10940  mulexpzap  10941  leexp1a  10956  faclbnd  11103  wrdeq  11246  ccatcl  11281  swrdsbslen  11358  swrdspsleq  11359  pfxccat1  11394  swrdswrdlem  11396  pfxccatin12lem2a  11419  swrdccatin2  11421  pfxccatin12lem2  11423  swrdccat  11427  reuccatpfxs1  11439  rexanuz  11673  sqabsadd  11740  sqabssub  11741  abs2dif  11791  rpmincl  11923  xrminrpcl  11959  fsum2dlemstep  12120  fprodeq0  12303  fprod2dlemstep  12308  summodnegmod  12508  dvds2ln  12510  dvdsflip  12537  gcdsupex  12653  gcdsupcl  12654  gcdabs  12684  sqgcd  12725  nnwosdc  12735  lcmabs  12773  lcmgcdlem  12774  lcmgcd  12775  lcmgcdeq  12780  qredeq  12793  cncongr1  12800  cncongr2  12801  hashgcdlem  12935  dvdsprmpweqle  13035  difsqpwdvds  13036  xpsfrnel2  13559  fngsum  13601  igsumvalx  13602  mndissubm  13688  resmhm2  13701  grpissubg  13911  subrngpropd  14361  subrgpropd  14398  tgcl  14929  uncld  14978  innei  15028  cnco  15086  txbas  15123  txbasval  15132  blin2  15297  qtopbasss  15386  lgsmulsqcoprm  15919  gausslemma2dlem1a  15931  lgsquad2lem2  15955  umgredgprv  16110  uspgredg2v  16216  usgredg2v  16219  wlkeq  16349  uspgr2wlkeq2  16361  uspgr2wlkeqi  16362  clwwlknonex2  16434  bj-charfunbi  16581  bj-indind  16702