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  992  hban  1593  sbimi  1810  spsbbi  1890  2exeu  2170  cgsex2g  2836  cgsex4g  2837  spc2egv  2893  spc2gv  2894  sseq2  3248  unssin  3443  uneqin  3455  undif3ss  3465  prneimg  3852  ssunieq  3921  iuneq1  3978  iuneq2  3981  copsex2t  4331  soeq2  4407  tpexg  4535  eldifpw  4568  iunpw  4571  peano5  4690  opbrop  4798  xpsspw  4831  coeq1  4879  coeq2  4880  cnveq  4896  dmeq  4923  sotri  5124  elxp4  5216  elxp5  5217  funun  5362  fununfun  5364  fundif  5365  funtp  5374  imain  5403  2elresin  5434  funssxp  5493  fssres  5501  f1co  5543  foun  5591  resdif  5594  f1oco  5595  fvun1  5700  elfvmptrab1  5729  fvreseq  5738  ftpg  5823  f1o2ndf1  6374  spc2ed  6379  smores  6438  nnaord  6655  nnm00  6676  brecop  6772  eroveu  6773  ecopovtrn  6779  ecopovtrng  6782  th3qlem1  6784  th3q  6787  ixpeq2  6859  djuexb  7211  addcmpblnq  7554  mulcmpblnq  7555  mulclnq  7563  dmaddpq  7566  dmmulpq  7567  mulcanenq  7572  distrnqg  7574  ltdcnq  7584  ltexnqq  7595  enq0breq  7623  mulcmpblnq0  7631  mulcanenq0ec  7632  addnnnq0  7636  mulnnnq0  7637  mulclnq0  7639  nqpnq0nq  7640  nqnq0a  7641  nqnq0m  7642  distrnq0  7646  elinp  7661  genpml  7704  genpmu  7705  genprndl  7708  genprndu  7709  addnqprl  7716  addnqpru  7717  distrlem1prl  7769  distrlem1pru  7770  ltsopr  7783  cauappcvgprlemdisj  7838  caucvgprlemdisj  7861  caucvgprprlemdisj  7889  addcmpblnr  7926  addsrpr  7932  mulsrpr  7933  addclsr  7940  addasssrg  7943  0idsr  7954  1idsr  7955  00sr  7956  mulgt0sr  7965  axaddcl  8051  axmulcl  8053  axaddass  8059  axdistr  8061  cnegexlem3  8323  cnegex  8324  apirr  8752  recexaplem2  8799  zletric  9490  zlelttric  9491  difgtsumgt  9516  qaddcl  9830  qmulcl  9832  qreccl  9837  iccss  10137  fzsubel  10256  elfz0add  10316  difelfznle  10331  2ffzeq  10337  fzonmapblen  10387  ubmelfzo  10406  ubmelm1fzo  10432  subfzo0  10448  qletric  10461  qlelttric  10462  adddivflid  10512  mulexp  10800  mulexpzap  10801  leexp1a  10816  faclbnd  10963  wrdeq  11093  ccatcl  11128  swrdsbslen  11198  swrdspsleq  11199  pfxccat1  11234  swrdswrdlem  11236  pfxccatin12lem2a  11259  swrdccatin2  11261  pfxccatin12lem2  11263  swrdccat  11267  reuccatpfxs1  11279  rexanuz  11499  sqabsadd  11566  sqabssub  11567  abs2dif  11617  rpmincl  11749  xrminrpcl  11785  fsum2dlemstep  11945  fprodeq0  12128  fprod2dlemstep  12133  summodnegmod  12333  dvds2ln  12335  dvdsflip  12362  gcdsupex  12478  gcdsupcl  12479  gcdabs  12509  sqgcd  12550  nnwosdc  12560  lcmabs  12598  lcmgcdlem  12599  lcmgcd  12600  lcmgcdeq  12605  qredeq  12618  cncongr1  12625  cncongr2  12626  hashgcdlem  12760  dvdsprmpweqle  12860  difsqpwdvds  12861  xpsfrnel2  13379  fngsum  13421  igsumvalx  13422  mndissubm  13508  resmhm2  13521  grpissubg  13731  subrngpropd  14180  subrgpropd  14217  tgcl  14738  uncld  14787  innei  14837  cnco  14895  txbas  14932  txbasval  14941  blin2  15106  qtopbasss  15195  lgsmulsqcoprm  15725  gausslemma2dlem1a  15737  lgsquad2lem2  15761  umgredgprv  15915  uspgredg2v  16019  usgredg2v  16022  wlkeq  16065  uspgr2wlkeq2  16077  uspgr2wlkeqi  16078  bj-charfunbi  16174  bj-indind  16295