Theorem anim12i 613

Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)

Hypotheses

Ref	Expression
anim12i.1	⊢ (𝜑 → 𝜓)
anim12i.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
anim12i	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Proof of Theorem anim12i

Step	Hyp	Ref	Expression
1		anim12i.1	. 2 ⊢ (𝜑 → 𝜓)
2		anim12i.2	. 2 ⊢ (𝜒 → 𝜃)
3		id 22	. 2 ⊢ ((𝜓 ∧ 𝜃) → (𝜓 ∧ 𝜃))
4	1, 2, 3	syl2an 596	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  anim12ci  614  anim1i  615  anim2i  617  anifp  1071  cgsex2g  3486  cgsex4g  3487  cgsex4gOLD  3488  spc2egv  3553  spc2ed  3555  uneqin  4241  2reu4lem  4476  2reu4  4477  disjpr2  4670  ssunieq  4899  iuneq1  4963  iuneq2  4966  copsex2t  5440  propeqop  5455  opthhausdorff  5465  opthhausdorff0  5466  iunopeqop  5469  soeq2  5554  opbrop  5722  xpsspw  5758  coeq1  5806  coeq2  5807  cnveq  5822  dmeq  5852  sotri  6084  tz7.7  6343  funun  6538  fununfun  6540  fundif  6541  funprg  6546  funtp  6549  2elresin  6613  funssxp  6690  fssres  6700  f1cof1  6740  foun  6792  f1un  6794  resdif  6795  f1oco  6797  fvun  6924  elfvmptrab1w  6968  elfvmptrab1  6969  fvn0ssdmfun  7019  dff3  7045  exfo  7050  fprg  7100  ftpg  7101  f1ounsn  7218  weisoeq2  7302  oprabv  7418  ndmovdistr  7547  ndmovord  7548  brrpssg  7670  eldifpw  7713  iunpw  7716  epweon  7720  bropfvvvv  8034  f1o2ndf1  8064  poseq  8100  fvn0elsupp  8122  smores  8284  tz7.49  8376  tz7.49c  8377  oaord  8474  oeeulem  8529  nnaord  8547  brecop  8747  brecop2  8748  eroveu  8749  ecopovtrn  8757  ixpeq2  8849  undifixp  8872  sbthlem8  9022  sbthlem9  9023  unxpdom  9159  isinf  9165  f1opwfi  9256  fiin  9325  en2lp  9515  inf3lem3  9539  brttrcl  9622  tcmin  9648  djuexb  9821  alephfp  10018  kmlem16  10076  endjudisj  10079  cofsmo  10179  fin23lem28  10250  axdc3lem2  10361  ac6c4  10391  brdom3  10438  brdom5  10439  brdom4  10440  canthp1lem2  10564  finngch  10566  ordpipq  10853  adderpq  10867  mulerpq  10868  lterpq  10881  genpn0  10914  genpnnp  10916  addclprlem2  10928  addcmpblnr  10980  addsrpr  10986  mulsrpr  10987  addclsr  10994  addasssr  10999  distrsr  11002  0idsr  11008  1idsr  11009  00sr  11010  mulgt0sr  11016  axaddf  11056  axaddass  11067  axdistr  11069  cnegex  11314  recextlem2  11768  difgtsumgt  12454  zaddcl  12531  qaddcl  12878  qmulcl  12880  qreccl  12882  xmulgt0  13198  xrsupsslem  13222  xrinfmsslem  13223  supxrpnf  13233  iccss  13330  difreicc  13400  fzadd2  13475  fzsubel  13476  ssfzunsnext  13485  difelfznle  13558  2ffzeq  13565  nelfzo  13580  fzonmapblen  13624  ubmelfzo  13646  ubmelm1fzo  13679  elfznelfzo  13689  subfzo0  13708  adddivflid  13738  modaddid  13830  modifeq2int  13856  modaddmodup  13857  addmodlteq  13869  fsuppmapnn0fiub  13914  mulexp  14024  mulexpz  14025  leexp1a  14098  faclbnd  14213  hashunx  14309  hashgt23el  14347  wrdeq  14459  ccatcl  14497  swrdnd  14578  swrdnd0  14581  swrdsbslen  14588  swrdspsleq  14589  pfxccat1  14625  swrdswrdlem  14627  pfxccatin12lem2a  14650  swrdccatin2  14652  pfxccatin12lem2  14654  pfxccatin12  14656  swrdccat  14658  reuccatpfxs1  14670  repswswrd  14707  repswccat  14709  cshwidxn  14732  cshweqdif2  14742  2cshwcshw  14748  cshwcshid  14750  cshwcsh2id  14751  f1oun2prg  14840  s2eq2s1eq  14859  s3eqs2s1eq  14861  s3sndisj  14890  s3iunsndisj  14891  sqabsadd  15205  sqabssub  15206  abs2dif  15256  rexanuz  15269  o1of2  15536  o1rlimmul  15542  fsum2dlem  15693  isumltss  15771  fprodser  15872  fprodeq0  15898  fprod2dlem  15903  dvdscmulr  16211  dvdsmulcr  16212  summodnegmod  16213  difmod0  16214  dvds2ln  16216  dvdsflip  16244  divalglem9  16328  gcdcllem3  16428  gcdaddmlem  16451  sqgcd  16489  lcmcllem  16523  lcmabs  16532  lcmgcdlem  16533  lcmgcd  16534  lcmgcdeq  16539  lcmftp  16563  lcmfunsnlem2lem1  16565  qredeq  16584  cncongr1  16594  cncongr2  16595  isprm7  16635  hashgcdlem  16715  dvdsprmpweqle  16814  difsqpwdvds  16815  prmgaplem4  16982  cshwsidrepsw  17021  setsfun0  17099  setsstruct2  17101  xpsfrnel2  17485  isfunc  17788  tsrss  18512  chnpof1  18553  rabsubmgmd  18629  resmgmhm2  18637  mndpfsupp  18692  ismhm0  18715  mhmismgmhm  18716  mndissubm  18732  resmndismnd  18733  resmhm2  18746  submefmnd  18820  sursubmefmnd  18821  injsubmefmnd  18822  grpissubg  19076  gimco  19197  symg2bas  19322  pgrpsubgsymg  19338  symgextf  19346  fvcosymgeq  19358  gsmsymgreqlem1  19359  symgfixf1  19366  efgrelexlema  19678  gsum2dlem1  19899  gsum2dlem2  19900  dvdsr  20298  isrnghmmul  20378  c0ghm  20397  rhmisrnghm  20416  subrngpropd  20501  subrgpropd  20541  rnghmsubcsetclem2  20565  rngcinv  20570  rhmsubcsetclem2  20594  rhmsubcrngclem2  20600  ringcinv  20604  srhmsubc  20613  islmhm2  20990  psgnghm  21535  psgndiflemB  21555  frlmbas3  21731  frlmphl  21736  islindf4  21793  ressmpladd  21984  ressmplmul  21985  mplind  22025  mpomatmul  22390  mavmul0g  22497  1marepvsma1  22527  mdetdiag  22543  slesolvec  22623  cramerimplem2  22628  cramerimplem3  22629  cramerimp  22630  mat2pmatlin  22679  m2pmfzgsumcl  22692  monmatcollpw  22723  pmatcollpw3lem  22727  pmatcollpwscmatlem1  22733  chpmat1dlem  22779  chfacfisf  22798  chfacfisfcpmat  22799  chfacfpmmulgsum2  22809  tgcl  22913  uncld  22985  innei  23069  cnco  23210  uncmp  23347  txbas  23511  txbasval  23550  tx1stc  23594  fbun  23784  infil  23807  fbunfip  23813  filuni  23829  imaelfm  23895  txflf  23950  tsmsfbas  24072  tsmsxp  24099  blin2  24373  nmhmplusg  24701  qtopbaslem  24702  iccntr  24766  ncvspi  25112  ncvs1  25113  unmbl  25494  volfiniun  25504  mbfi1flimlem  25679  ply1idom  26086  logreclem  26728  relogbcxpb  26753  fsumvma2  27181  chpchtsum  27186  dchrelbas3  27205  dchrmulcl  27216  lgsmulsqcoprm  27310  gausslemma2dlem1a  27332  lgsquad2lem2  27352  dchrisum0fmul  27473  dchrisum0lem1  27483  ltsres  27630  nocvxminlem  27750  oldlim  27883  madebdayim  27884  madebdaylemlrcut  27895  readdscl  28495  remulscl  28498  ishpg  28831  brcgr  28973  brbtwn2  28978  axcontlem2  29038  uspgredg2v  29297  usgredg2v  29300  usgr2v1e2w  29325  nb3gr2nb  29457  cusgredg  29497  cplgr3v  29508  cusgrop  29511  rusgr1vtx  29662  iswlkg  29687  wlkeq  29707  wlk1walk  29712  uspgr2wlkeq2  29720  uspgr2wlkeqi  29721  cyclnumvtx  29873  crctcshwlkn0lem3  29885  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  wspthneq1eq2  29933  wwlksnextinj  29972  2wlkdlem7  30005  2wlkdlem8  30006  2pthon3v  30016  s3wwlks2on  30029  sps3wwlks2on  30030  elwwlks2  30042  elwspths2spth  30043  rusgrnumwwlks  30050  clwlkclwwlklem2a  30073  clwlkclwwlklem3  30076  clwlkclwwlkf1lem2  30080  clwlkclwwlkf1  30085  clwwlknonex2  30184  3wlkdlem3  30236  uhgr3cyclex  30257  cusconngr  30266  eupth0  30289  frgr3v  30350  1to3vfriswmgr  30355  4cycl2v2nb  30364  frgrnbnb  30368  frgrncvvdeq  30384  frgrwopreglem4a  30385  frgrwopreglem5a  30386  frgrwopreglem4  30390  frgrwopreglem5  30396  frgrhash2wsp  30407  numclwwlk1lem2foa  30429  numclwwlk2  30456  blocni  30880  hvsub4  31112  shscli  31392  shscom  31394  spanunsni  31654  spanpr  31655  5oalem2  31730  5oalem3  31731  5oalem5  31733  3oalem1  31737  hoscl  31820  hoadddi  31878  hoadddir  31879  hosub4  31888  lnophsi  32076  hmops  32095  hmopm  32096  adjadd  32168  leop2  32199  leopadd  32207  leopmuli  32208  pjclem4  32274  pj3si  32282  mdslmd1lem2  32401  mdslmd3i  32407  atomli  32457  atcvatlem  32460  chirredlem3  32467  chirredi  32469  atcvat3i  32471  mdsymlem1  32478  mdsymlem5  32482  cdjreui  32507  cdj3i  32516  addltmulALT  32521  hashxpe  32887  domnmuln0rd  33356  mndpluscn  34083  sxbrsigalem5  34445  probfinmeasbALTV  34586  bnj545  35051  bnj546  35052  bnj557  35057  bnj570  35061  bnj594  35068  bnj1001  35115  bnj1118  35140  txpconn  35426  cvmlift2lem10  35506  gonar  35589  lediv2aALT  35871  altopeq12  36156  altxpsspw  36171  funtransport  36225  neibastop1  36553  filnetlem3  36574  lukshef-ax2  36609  arg-ax  36610  nndivsub  36651  bj-nnftht  36942  bj-nnfan  36949  bj-nnfor  36951  copsex2b  37345  isbasisrelowllem1  37560  isbasisrelowllem2  37561  icoreclin  37562  relowlssretop  37568  rdgeqoa  37575  fvineqsnf1  37615  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem4  37825  poimirlem26  37847  poimirlem29  37850  poimirlem30  37851  heicant  37856  mblfinlem1  37858  ismblfin  37862  itg2addnclem  37872  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  prdstotbnd  37995  heibor1lem  38010  isdrngo2  38159  divrngidl  38229  pridlc3  38274  linepsubN  40012  pmapsub  40028  elpaddri  40062  paddasslem14  40093  pmapjoin  40112  dvhfvadd  41351  dvhvaddcomN  41356  bcle2d  42433  imacrhmcl  42769  rimco  42773  rmxynorm  43160  monotoddzzfi  43184  acongtr  43220  mpaaeu  43392  oaltublim  43532  omord2lim  43542  cantnftermord  43562  dflim5  43571  omabs2  43574  tfsconcat0i  43587  ofoafo  43598  naddcnff  43604  oaun3lem1  43616  oaun3lem2  43617  pr2cv  43789  brfvrcld2  43933  rfovcnvf1od  44245  ismnushort  44542  nzin  44559  pm10.14  44600  disjrnmpt2  45432  liminfvalxr  46027  etransclem38  46516  cfsetsnfsetf1  47305  tz6.12-afv2  47486  2elfz2melfz  47564  fz0addge0  47565  2ffzoeq  47573  difltmodne  47588  modn0mul  47603  mod2addne  47610  icceuelpartlem  47681  icceuelpart  47682  ich2exprop  47717  sqrtpwpw2p  47784  fmtnoprmfac1lem  47810  fmtnoprmfac1  47811  lighneallem2  47852  divgcdoddALTV  47928  gbowpos  48005  gbowgt5  48008  gboge9  48010  nnsum3primesgbe  48038  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  isuspgrim  48142  clnbgrgrimlem  48179  clnbgrgrim  48180  isgrtri  48189  isubgr3stgrlem4  48215  grlimgrtri  48249  grlictr  48261  gpgedgvtx0  48307  gpgedg2iv  48313  gpg5nbgrvtx03star  48326  gpg5nbgr3star  48327  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  pgn4cyclex  48372  isupwlkg  48383  rngcinvALTV  48522  ringcinvALTV  48556  srhmsubcALTV  48571  mapprop  48592  zlmodzxzadd  48604  domnmsuppn0  48615  ply1mulgsumlem2  48633  lincsum  48675  lincsumcl  48677  lincscmcl  48678  isldepslvec2  48731  digexp  48853  rrx2pnecoorneor  48961  rrx2pnedifcoorneorr  48963  rrx2xpref1o  48964  ehl2eudis0lt  48972  rrx2linest  48988  line2x  49000  itsclc0yqsollem2  49009  seppsepf  49174  thincn0eu  49676