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  1812  spsbbi  1892  2exeu  2172  cgsex2g  2840  cgsex4g  2841  spc2egv  2897  spc2gv  2898  sseq2  3252  unssin  3448  uneqin  3460  undif3ss  3470  prneimg  3862  ssunieq  3931  iuneq1  3988  iuneq2  3991  copsex2t  4343  soeq2  4419  tpexg  4547  eldifpw  4580  iunpw  4583  peano5  4702  opbrop  4811  xpsspw  4844  coeq1  4893  coeq2  4894  cnveq  4910  dmeq  4937  sotri  5139  elxp4  5231  elxp5  5232  funun  5378  fununfun  5380  fundif  5381  funtp  5390  imain  5419  2elresin  5450  funssxp  5512  fssres  5520  f1co  5563  foun  5611  resdif  5614  f1oco  5615  fvun1  5721  elfvmptrab1  5750  fvreseq  5759  ftpg  5846  f1o2ndf1  6402  spc2ed  6407  fvn0elsupp  6429  smores  6501  nnaord  6720  nnm00  6741  brecop  6837  eroveu  6838  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  th3q  6852  ixpeq2  6924  djuexb  7303  addcmpblnq  7647  mulcmpblnq  7648  mulclnq  7656  dmaddpq  7659  dmmulpq  7660  mulcanenq  7665  distrnqg  7667  ltdcnq  7677  ltexnqq  7688  enq0breq  7716  mulcmpblnq0  7724  mulcanenq0ec  7725  addnnnq0  7729  mulnnnq0  7730  mulclnq0  7732  nqpnq0nq  7733  nqnq0a  7734  nqnq0m  7735  distrnq0  7739  elinp  7754  genpml  7797  genpmu  7798  genprndl  7801  genprndu  7802  addnqprl  7809  addnqpru  7810  distrlem1prl  7862  distrlem1pru  7863  ltsopr  7876  cauappcvgprlemdisj  7931  caucvgprlemdisj  7954  caucvgprprlemdisj  7982  addcmpblnr  8019  addsrpr  8025  mulsrpr  8026  addclsr  8033  addasssrg  8036  0idsr  8047  1idsr  8048  00sr  8049  mulgt0sr  8058  axaddcl  8144  axmulcl  8146  axaddass  8152  axdistr  8154  cnegexlem3  8415  cnegex  8416  apirr  8844  recexaplem2  8891  zletric  9584  zlelttric  9585  difgtsumgt  9610  qaddcl  9930  qmulcl  9932  qreccl  9937  iccss  10237  fzsubel  10357  elfz0add  10417  difelfznle  10432  2ffzeq  10438  fzonmapblen  10489  ubmelfzo  10508  ubmelm1fzo  10534  subfzo0  10551  qletric  10564  qlelttric  10565  adddivflid  10615  mulexp  10903  mulexpzap  10904  leexp1a  10919  faclbnd  11066  wrdeq  11201  ccatcl  11236  swrdsbslen  11313  swrdspsleq  11314  pfxccat1  11349  swrdswrdlem  11351  pfxccatin12lem2a  11374  swrdccatin2  11376  pfxccatin12lem2  11378  swrdccat  11382  reuccatpfxs1  11394  rexanuz  11628  sqabsadd  11695  sqabssub  11696  abs2dif  11746  rpmincl  11878  xrminrpcl  11914  fsum2dlemstep  12075  fprodeq0  12258  fprod2dlemstep  12263  summodnegmod  12463  dvds2ln  12465  dvdsflip  12492  gcdsupex  12608  gcdsupcl  12609  gcdabs  12639  sqgcd  12680  nnwosdc  12690  lcmabs  12728  lcmgcdlem  12729  lcmgcd  12730  lcmgcdeq  12735  qredeq  12748  cncongr1  12755  cncongr2  12756  hashgcdlem  12890  dvdsprmpweqle  12990  difsqpwdvds  12991  xpsfrnel2  13509  fngsum  13551  igsumvalx  13552  mndissubm  13638  resmhm2  13651  grpissubg  13861  subrngpropd  14311  subrgpropd  14348  tgcl  14875  uncld  14924  innei  14974  cnco  15032  txbas  15069  txbasval  15078  blin2  15243  qtopbasss  15332  lgsmulsqcoprm  15865  gausslemma2dlem1a  15877  lgsquad2lem2  15901  umgredgprv  16056  uspgredg2v  16162  usgredg2v  16165  wlkeq  16295  uspgr2wlkeq2  16307  uspgr2wlkeqi  16308  clwwlknonex2  16380  bj-charfunbi  16527  bj-indind  16648