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  994  hban  1595  sbimi  1812  spsbbi  1892  2exeu  2172  cgsex2g  2839  cgsex4g  2840  spc2egv  2896  spc2gv  2897  sseq2  3251  unssin  3446  uneqin  3458  undif3ss  3468  prneimg  3857  ssunieq  3926  iuneq1  3983  iuneq2  3986  copsex2t  4337  soeq2  4413  tpexg  4541  eldifpw  4574  iunpw  4577  peano5  4696  opbrop  4805  xpsspw  4838  coeq1  4887  coeq2  4888  cnveq  4904  dmeq  4931  sotri  5132  elxp4  5224  elxp5  5225  funun  5371  fununfun  5373  fundif  5374  funtp  5383  imain  5412  2elresin  5443  funssxp  5504  fssres  5512  f1co  5554  foun  5602  resdif  5605  f1oco  5606  fvun1  5712  elfvmptrab1  5741  fvreseq  5750  ftpg  5837  f1o2ndf1  6392  spc2ed  6397  smores  6457  nnaord  6676  nnm00  6697  brecop  6793  eroveu  6794  ecopovtrn  6800  ecopovtrng  6803  th3qlem1  6805  th3q  6808  ixpeq2  6880  djuexb  7242  addcmpblnq  7586  mulcmpblnq  7587  mulclnq  7595  dmaddpq  7598  dmmulpq  7599  mulcanenq  7604  distrnqg  7606  ltdcnq  7616  ltexnqq  7627  enq0breq  7655  mulcmpblnq0  7663  mulcanenq0ec  7664  addnnnq0  7668  mulnnnq0  7669  mulclnq0  7671  nqpnq0nq  7672  nqnq0a  7673  nqnq0m  7674  distrnq0  7678  elinp  7693  genpml  7736  genpmu  7737  genprndl  7740  genprndu  7741  addnqprl  7748  addnqpru  7749  distrlem1prl  7801  distrlem1pru  7802  ltsopr  7815  cauappcvgprlemdisj  7870  caucvgprlemdisj  7893  caucvgprprlemdisj  7921  addcmpblnr  7958  addsrpr  7964  mulsrpr  7965  addclsr  7972  addasssrg  7975  0idsr  7986  1idsr  7987  00sr  7988  mulgt0sr  7997  axaddcl  8083  axmulcl  8085  axaddass  8091  axdistr  8093  cnegexlem3  8355  cnegex  8356  apirr  8784  recexaplem2  8831  zletric  9522  zlelttric  9523  difgtsumgt  9548  qaddcl  9868  qmulcl  9870  qreccl  9875  iccss  10175  fzsubel  10294  elfz0add  10354  difelfznle  10369  2ffzeq  10375  fzonmapblen  10425  ubmelfzo  10444  ubmelm1fzo  10470  subfzo0  10487  qletric  10500  qlelttric  10501  adddivflid  10551  mulexp  10839  mulexpzap  10840  leexp1a  10855  faclbnd  11002  wrdeq  11134  ccatcl  11169  swrdsbslen  11246  swrdspsleq  11247  pfxccat1  11282  swrdswrdlem  11284  pfxccatin12lem2a  11307  swrdccatin2  11309  pfxccatin12lem2  11311  swrdccat  11315  reuccatpfxs1  11327  rexanuz  11548  sqabsadd  11615  sqabssub  11616  abs2dif  11666  rpmincl  11798  xrminrpcl  11834  fsum2dlemstep  11994  fprodeq0  12177  fprod2dlemstep  12182  summodnegmod  12382  dvds2ln  12384  dvdsflip  12411  gcdsupex  12527  gcdsupcl  12528  gcdabs  12558  sqgcd  12599  nnwosdc  12609  lcmabs  12647  lcmgcdlem  12648  lcmgcd  12649  lcmgcdeq  12654  qredeq  12667  cncongr1  12674  cncongr2  12675  hashgcdlem  12809  dvdsprmpweqle  12909  difsqpwdvds  12910  xpsfrnel2  13428  fngsum  13470  igsumvalx  13471  mndissubm  13557  resmhm2  13570  grpissubg  13780  subrngpropd  14229  subrgpropd  14266  tgcl  14787  uncld  14836  innei  14886  cnco  14944  txbas  14981  txbasval  14990  blin2  15155  qtopbasss  15244  lgsmulsqcoprm  15774  gausslemma2dlem1a  15786  lgsquad2lem2  15810  umgredgprv  15965  uspgredg2v  16071  usgredg2v  16074  wlkeq  16204  uspgr2wlkeq2  16216  uspgr2wlkeqi  16217  clwwlknonex2  16289  bj-charfunbi  16406  bj-indind  16527