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  1561  sbimi  1778  spsbbi  1858  2exeu  2137  cgsex2g  2799  cgsex4g  2800  spc2egv  2854  spc2gv  2855  sseq2  3207  unssin  3402  uneqin  3414  undif3ss  3424  prneimg  3804  ssunieq  3872  iuneq1  3929  iuneq2  3932  copsex2t  4278  soeq2  4351  tpexg  4479  eldifpw  4512  iunpw  4515  peano5  4634  opbrop  4742  xpsspw  4775  coeq1  4823  coeq2  4824  cnveq  4840  dmeq  4866  sotri  5065  elxp4  5157  elxp5  5158  funun  5302  funtp  5311  imain  5340  2elresin  5369  funssxp  5427  fssres  5433  f1co  5475  foun  5523  resdif  5526  f1oco  5527  fvun1  5627  elfvmptrab1  5656  fvreseq  5665  ftpg  5746  f1o2ndf1  6286  spc2ed  6291  smores  6350  nnaord  6567  nnm00  6588  brecop  6684  eroveu  6685  ecopovtrn  6691  ecopovtrng  6694  th3qlem1  6696  th3q  6699  ixpeq2  6771  djuexb  7110  addcmpblnq  7434  mulcmpblnq  7435  mulclnq  7443  dmaddpq  7446  dmmulpq  7447  mulcanenq  7452  distrnqg  7454  ltdcnq  7464  ltexnqq  7475  enq0breq  7503  mulcmpblnq0  7511  mulcanenq0ec  7512  addnnnq0  7516  mulnnnq0  7517  mulclnq0  7519  nqpnq0nq  7520  nqnq0a  7521  nqnq0m  7522  distrnq0  7526  elinp  7541  genpml  7584  genpmu  7585  genprndl  7588  genprndu  7589  addnqprl  7596  addnqpru  7597  distrlem1prl  7649  distrlem1pru  7650  ltsopr  7663  cauappcvgprlemdisj  7718  caucvgprlemdisj  7741  caucvgprprlemdisj  7769  addcmpblnr  7806  addsrpr  7812  mulsrpr  7813  addclsr  7820  addasssrg  7823  0idsr  7834  1idsr  7835  00sr  7836  mulgt0sr  7845  axaddcl  7931  axmulcl  7933  axaddass  7939  axdistr  7941  cnegexlem3  8203  cnegex  8204  apirr  8632  recexaplem2  8679  zletric  9370  zlelttric  9371  difgtsumgt  9395  qaddcl  9709  qmulcl  9711  qreccl  9716  iccss  10016  fzsubel  10135  elfz0add  10195  difelfznle  10210  2ffzeq  10216  fzonmapblen  10263  ubmelfzo  10276  ubmelm1fzo  10302  subfzo0  10318  qletric  10331  qlelttric  10332  adddivflid  10382  mulexp  10670  mulexpzap  10671  leexp1a  10686  faclbnd  10833  wrdeq  10957  rexanuz  11153  sqabsadd  11220  sqabssub  11221  abs2dif  11271  rpmincl  11403  xrminrpcl  11439  fsum2dlemstep  11599  fprodeq0  11782  fprod2dlemstep  11787  summodnegmod  11987  dvds2ln  11989  dvdsflip  12016  gcdsupex  12124  gcdsupcl  12125  gcdabs  12155  sqgcd  12196  nnwosdc  12206  lcmabs  12244  lcmgcdlem  12245  lcmgcd  12246  lcmgcdeq  12251  qredeq  12264  cncongr1  12271  cncongr2  12272  hashgcdlem  12406  dvdsprmpweqle  12506  difsqpwdvds  12507  xpsfrnel2  12989  fngsum  13031  igsumvalx  13032  mndissubm  13107  resmhm2  13120  grpissubg  13324  subrngpropd  13772  subrgpropd  13809  tgcl  14300  uncld  14349  innei  14399  cnco  14457  txbas  14494  txbasval  14503  blin2  14668  qtopbasss  14757  lgsmulsqcoprm  15287  gausslemma2dlem1a  15299  lgsquad2lem2  15323  bj-charfunbi  15457  bj-indind  15578