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  999  hban  1600  sbimi  1817  spsbbi  1897  2exeu  2179  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  sseq2  3272  unssin  3470  uneqin  3482  undif3ss  3492  prneimg  3894  ssunieq  3963  iuneq1  4020  iuneq2  4023  copsex2t  4380  soeq2  4456  tpexg  4585  eldifpw  4618  iunpw  4621  peano5  4740  opbrop  4849  xpsspw  4882  coeq1  4932  coeq2  4933  cnveq  4949  dmeq  4976  sotri  5178  elxp4  5270  elxp5  5271  funun  5417  fununfun  5419  fundif  5420  funtp  5429  imain  5458  2elresin  5489  funssxp  5552  fssres  5560  f1co  5605  foun  5653  resdif  5656  f1oco  5657  fvun1  5763  elfvmptrab1  5794  fvreseq  5803  ftpg  5890  f1o2ndf1  6454  spc2ed  6459  fvn0elsupp  6481  smores  6553  nnaord  6772  nnm00  6793  brecop  6889  eroveu  6890  ecopovtrn  6896  ecopovtrng  6899  th3qlem1  6901  th3q  6904  ixpeq2  6984  djuexb  7374  addcmpblnq  7724  mulcmpblnq  7725  mulclnq  7733  dmaddpq  7736  dmmulpq  7737  mulcanenq  7742  distrnqg  7744  ltdcnq  7754  ltexnqq  7765  enq0breq  7793  mulcmpblnq0  7801  mulcanenq0ec  7802  addnnnq0  7806  mulnnnq0  7807  mulclnq0  7809  nqpnq0nq  7810  nqnq0a  7811  nqnq0m  7812  distrnq0  7816  elinp  7831  genpml  7874  genpmu  7875  genprndl  7878  genprndu  7879  addnqprl  7886  addnqpru  7887  distrlem1prl  7939  distrlem1pru  7940  ltsopr  7953  cauappcvgprlemdisj  8008  caucvgprlemdisj  8031  caucvgprprlemdisj  8059  addcmpblnr  8096  addsrpr  8102  mulsrpr  8103  addclsr  8110  addasssrg  8113  0idsr  8124  1idsr  8125  00sr  8126  mulgt0sr  8135  axaddcl  8221  axmulcl  8223  axaddass  8229  axdistr  8231  cnegexlem3  8493  cnegex  8494  apirr  8923  recexaplem2  8970  zletric  9667  zlelttric  9668  difgtsumgt  9693  qaddcl  10014  qmulcl  10016  qreccl  10021  iccss  10322  fzsubel  10444  elfz0add  10505  difelfznle  10520  2ffzeq  10526  fzonmapblen  10577  ubmelfzo  10596  ubmelm1fzo  10622  subfzo0  10639  qletric  10654  qlelttric  10655  adddivflid  10705  mulexp  10993  mulexpzap  10994  leexp1a  11009  faclbnd  11157  wrdeq  11304  ccatcl  11339  swrdsbslen  11416  swrdspsleq  11417  pfxccat1  11452  swrdswrdlem  11454  pfxccatin12lem2a  11477  swrdccatin2  11479  pfxccatin12lem2  11481  swrdccat  11485  reuccatpfxs1  11497  rexanuz  11732  sqabsadd  11799  sqabssub  11800  abs2dif  11850  rpmincl  11982  xrminrpcl  12018  fsum2dlemstep  12179  fprodeq0  12362  fprod2dlemstep  12367  summodnegmod  12567  dvds2ln  12569  dvdsflip  12596  gcdsupex  12712  gcdsupcl  12713  gcdabs  12743  sqgcd  12784  nnwosdc  12794  lcmabs  12832  lcmgcdlem  12833  lcmgcd  12834  lcmgcdeq  12839  qredeq  12852  cncongr1  12859  cncongr2  12860  hashgcdlem  12994  dvdsprmpweqle  13094  difsqpwdvds  13095  xpsfrnel2  13644  fngzsum  13685  gzsumvalx  13686  mndissubm  13759  resmhm2  13772  grpissubg  13974  subrngpropd  14497  subrgpropd  14534  tgcl  15088  uncld  15137  innei  15187  cnco  15245  txbas  15282  txbasval  15291  blin2  15456  qtopbasss  15545  lgsmulsqcoprm  16079  gausslemma2dlem1a  16091  lgsquad2lem2  16115  umgredgprv  16270  uspgredg2v  16376  usgredg2v  16379  wlkeq  16509  uspgr2wlkeq2  16521  uspgr2wlkeqi  16522  clwwlknonex2  16594  bj-charfunbi  16751  bj-indind  16872