Theorem anim12i 588

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 493	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anim12ci  589  anim1i  590  anim2i  591  anifp  1014  sbimi  1873  cgsex2g  3212  cgsex4g  3213  spc2egv  3268  sseq2  3590  uneqin  3837  undif3OLD  3848  disjpr2  4194  ssunieq  4408  iuneq1  4470  iuneq2  4473  copsex2t  4883  propeqop  4895  iunopeqop  4906  soeq2  4979  opbrop  5121  xpsspw  5156  coeq1  5201  coeq2  5202  cnveq  5218  dmeq  5246  sotri  5442  tz7.7  5666  funun  5846  fununfun  5848  fundif  5849  funprg  5854  funtp  5859  funcnvqpOLD  5867  2elresin  5916  funssxp  5974  fssres  5983  f1co  6023  foun  6068  resdif  6070  f1oco  6072  fvun  6178  elfvmptrab1  6213  fvn0ssdmfun  6258  dff3  6280  exfo  6285  fprg  6327  ftpg  6328  weisoeq2  6506  oprabv  6601  ndmovdistr  6721  ndmovord  6722  brrpssg  6837  eldifpw  6868  iunpw  6870  bropfvvvv  7144  f1o2ndf1  7172  fvn0elsupp  7198  wfrlem5  7306  smores  7336  tz7.49  7427  tz7.49c  7428  oaord  7514  oeeulem  7568  nnaord  7586  brecop  7727  brecop2  7728  eroveu  7729  ecopovtrn  7737  ixpeq2  7808  undifixp  7830  undom  7933  sbthlem8  7962  sbthlem9  7963  unxpdom  8052  isinf  8058  f1opwfi  8153  fiin  8211  en2lp  8393  inf3lem3  8410  tcmin  8500  alephfp  8814  kmlem16  8870  cdaval  8875  cdaun  8877  cofsmo  8974  fin23lem28  9045  axdc3lem2  9156  ac6c4  9186  brdom3  9231  brdom5  9232  brdom4  9233  canthp1lem2  9354  finngch  9356  ordpipq  9643  adderpq  9657  mulerpq  9658  lterpq  9671  genpn0  9704  genpnnp  9706  addclprlem2  9718  addcmpblnr  9769  addsrpr  9775  mulsrpr  9776  addclsr  9783  addasssr  9788  distrsr  9791  0idsr  9797  1idsr  9798  00sr  9799  mulgt0sr  9805  axaddf  9845  axaddass  9856  axdistr  9858  cnegex  10096  recextlem2  10537  difgtsumgt  11223  zaddcl  11294  qaddcl  11680  qmulcl  11682  qreccl  11684  xmulgt0  11985  xrsupsslem  12009  xrinfmsslem  12010  supxrpnf  12020  iccss  12112  difreicc  12175  fzadd2  12247  fzsubel  12248  ssfzunsn  12257  elfz0add  12307  difelfznle  12322  2ffzeq  12329  nelfzo  12344  fzonmapblen  12381  ubmelfzo  12400  ubmelm1fzo  12430  elfznelfzo  12439  subfzo0  12452  adddivflid  12481  modifeq2int  12594  modaddmodup  12595  addmodlteq  12607  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  mulexp  12761  mulexpz  12762  leexp1a  12781  faclbnd  12939  hashunx  13036  wrdeq  13182  ccatcl  13212  swrdnd  13284  swrdeq  13296  swrdsbslen  13300  swrdspsleq  13301  swrdswrdlem  13311  reuccats1  13332  swrdccatin12lem2a  13336  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12  13342  swrdccat  13344  repswswrd  13382  repswccat  13383  cshwidxn  13406  cshweqdif2  13416  2cshwcshw  13422  cshwcshid  13424  cshwcsh2id  13425  f1oun2prg  13512  s2eq2s1eq  13531  wwlktovf1  13548  s3sndisj  13554  s3iunsndisj  13555  sqabsadd  13870  sqabssub  13871  abs2dif  13920  rexanuz  13933  o1of2  14191  o1rlimmul  14197  fsum2dlem  14343  isumltss  14419  fprodser  14518  fprodeq0  14544  fprod2dlem  14549  dvdscmulr  14848  dvdsmulcr  14849  summodnegmod  14850  dvds2ln  14852  dvdsflip  14877  divalglem9  14962  gcdcllem3  15061  gcdaddmlem  15083  gcdabs  15088  sqgcd  15116  lcmcllem  15147  lcmabs  15156  lcmgcdlem  15157  lcmgcd  15158  lcmgcdeq  15163  lcmf  15184  lcmftp  15187  lcmfunsnlem2lem1  15189  qredeq  15209  cncongr1  15219  cncongr2  15220  isprm7  15258  divgcdodd  15260  hashgcdlem  15331  pythagtriplem19  15376  dvdsprmpweqle  15428  difsqpwdvds  15429  prmgaplem4  15596  cshwsidrepsw  15638  setsfun0  15726  setsstruct  15727  xpsfrnel2  16048  isfunc  16347  fpwipodrs  16987  tsrss  17046  resmhm2  17183  gimco  17533  symg2bas  17641  pgrpsubgsymg  17651  symgextf  17660  gsmsymgrfixlem1  17670  fvcosymgeq  17672  gsmsymgreqlem1  17673  symgfixf1  17680  efgrelexlema  17985  gsum2dlem1  18192  gsum2dlem2  18193  dvdsr  18469  subrgpropd  18637  islmhm2  18859  ressmpladd  19278  ressmplmul  19279  mplind  19323  psgnghm  19745  psgndiflemB  19765  frlmbas3  19934  frlmphl  19939  islindf4  19996  mpt2matmul  20071  mavmul0g  20178  1marepvsma1  20208  mdetdiag  20224  slesolvec  20304  cramerimplem2  20309  cramerimplem3  20310  cramerimp  20311  mat2pmatlin  20359  m2pmfzgsumcl  20372  monmatcollpw  20403  pmatcollpw3lem  20407  pmatcollpwscmatlem1  20413  chpmat1dlem  20459  chfacfisf  20478  chfacfisfcpmat  20479  chfacfpmmulgsum2  20489  tgcl  20584  uncld  20655  innei  20739  cnco  20880  uncmp  21016  txbas  21180  txbasval  21219  tx1stc  21263  fbun  21454  infil  21477  fbunfip  21483  filuni  21499  imaelfm  21565  txflf  21620  tsmsfbas  21741  tsmsxp  21768  blin2  22044  nmhmplusg  22371  qtopbaslem  22372  iccntr  22432  ncvspi  22764  ncvs1  22765  unmbl  23112  volfiniun  23122  mbfi1flimlem  23295  ply1idom  23688  logreclem  24300  relogbcxpb  24325  fsumvma2  24739  chpchtsum  24744  dchrelbas3  24763  dchrmulcl  24774  lgsmulsqcoprm  24868  gausslemma2dlem1a  24890  lgsquad2lem2  24910  dchrisum0fmul  24995  dchrisum0lem1  25005  ishpg  25451  brcgr  25580  brbtwn2  25585  axcontlem2  25645  usgraidx2v  25922  nb3gra2nb  25984  sizeusglecusg  26014  redwlk  26136  wlkdvspthlem  26137  usgra2adedgwlkon  26143  usgra2wlkspthlem1  26147  constr3lem6  26177  constr3trllem2  26179  cusconngra  26204  2wlkeq  26235  usg2wlkeq2  26237  wwlkextinj  26258  clwlkisclwwlklem2a  26313  clwlkisclwwlklem0  26316  clwwisshclww  26335  clwlkf1clwwlk  26377  el2wlkonotot0  26399  usg2spthonot0  26416  rusgranumwlkl1  26474  rusgra0edg  26482  iseupa  26492  frgra3v  26529  1to3vfriswmgra  26534  4cycl2v2nb  26543  frgranbnb  26547  frgrawopreg  26576  frg2woteqm  26586  2spotiundisj  26589  frghash2spot  26590  usg2spot2nb  26592  extwwlkfablem2  26605  numclwwlkovgelim  26616  numclwlk1lem2fo  26622  numclwwlk2  26634  frgrareggt1  26643  blocni  27044  hvsub4  27278  shscli  27560  shscom  27562  spanunsni  27822  spanpr  27823  5oalem2  27898  5oalem3  27899  5oalem5  27901  3oalem1  27905  hoscl  27988  hoadddi  28046  hoadddir  28047  hosub4  28056  lnophsi  28244  hmops  28263  hmopm  28264  adjadd  28336  leop2  28367  leopadd  28375  leopmuli  28376  pjclem4  28442  pj3si  28450  mdslmd1lem2  28569  mdslmd3i  28575  atomli  28625  atcvatlem  28628  chirredlem3  28635  chirredi  28637  atcvat3i  28639  mdsymlem1  28646  mdsymlem5  28650  cdjreui  28675  cdj3i  28684  addltmulALT  28689  spc2ed  28696  mndpluscn  29300  sxbrsigalem5  29677  probfinmeasbOLD  29817  bnj545  30219  bnj546  30220  bnj557  30225  bnj570  30229  bnj594  30236  bnj1001  30282  bnj1118  30306  txpcon  30468  cvmlift2lem10  30548  lediv2aALT  30825  poseq  30994  frrlem5  31028  sltres  31061  nocvxminlem  31089  altopeq12  31239  altxpsspw  31254  funtransport  31308  neibastop1  31524  filnetlem3  31545  lukshef-ax2  31584  arg-ax  31585  nndivsub  31626  isbasisrelowllem1  32379  isbasisrelowllem2  32380  icoreclin  32381  relowlssretop  32387  rdgeqoa  32394  wl-ax11-lem2  32542  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem4  32583  poimirlem26  32605  poimirlem29  32608  poimirlem30  32609  heicant  32614  mblfinlem1  32616  ismblfin  32620  itg2addnclem  32631  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  prdstotbnd  32763  heibor1lem  32778  isdrngo2  32927  divrngidl  32997  pridlc3  33042  linepsubN  34056  pmapsub  34072  elpaddri  34106  paddasslem14  34137  pmapjoin  34156  dvhfvadd  35398  dvhvaddcomN  35403  rmxynorm  36501  monotoddzzfi  36525  acongtr  36563  mpaaeu  36739  brfvrcld2  37003  rfovcnvf1od  37318  nzin  37539  pm10.14  37580  etransclem38  39165  2reu4a  39838  2reu4  39839  icceuelpartlem  39973  icceuelpart  39974  sqrtpwpw2p  39988  fmtnoprmfac1lem  40014  fmtnoprmfac1  40015  lighneallem2  40061  divgcdoddALTV  40131  gbopos  40181  gbogt5  40184  gboage9  40186  nnsum3primesgbe  40208  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  pfxeq  40267  pfxsuffeqwrdeq  40269  pfxccat1  40273  pfxccatin12lem2  40287  pfxccatin12  40288  2elfz2melfz  40355  fz0addge0  40356  2ffzoeq  40361  uhgruhgra  40375  uspgredg2v  40451  usgredg2v  40454  usgr2v1e2w  40478  nb3gr2nb  40612  cusgredg  40646  cplgr3v  40657  cusgrop  40660  rusgr1vtx  40788  is1wlkg  40816  1wlkeq  40838  1wlk1walk  40843  uspgr2wlkeq2  40855  uspgr2wlkeqi  40856  usgr2wlkneq  40962  usgr2pth  40970  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  wspthneq1eq2  41056  wlkwwlkfun  41092  wwlksnextinj  41105  21wlkdlem7  41139  21wlkdlem8  41140  2pthon3v-av  41150  s3wwlks2on  41160  elwwlks2  41170  elwspths2spth  41171  rusgrnumwwlks  41177  clwwlknp  41195  clwlkclwwlklem2a  41207  clwlkclwwlklem3  41210  clwlksf1clwwlk  41276  31wlkdlem3  41328  uhgr3cyclex  41349  cusconngr  41358  eupth0  41382  frgr3v  41445  1to3vfriswmgr  41450  4cycl2v2nb-av  41459  frgrnbnb  41463  frgrncvvdeq  41480  frgrwopreg  41486  frgrhash2wsp  41497  av-numclwlk1lem2fo  41525  av-numclwwlk2lem1  41532  av-numclwwlk2  41537  rabsubmgmd  41581  resmgmhm2  41589  ismhm0  41595  mhmismgmhm  41596  isrnghmmul  41683  c0ghm  41701  rhmisrnghm  41710  rnghmsubcsetclem2  41768  rngcinv  41773  rngcinvALTV  41785  rhmsubcsetclem2  41814  rhmsubcrngclem2  41820  ringcinv  41824  ringcinvALTV  41848  srhmsubc  41868  srhmsubcALTV  41887  mapprop  41917  zlmodzxzadd  41929  domnmsuppn0  41944  mndpfsupp  41951  ply1mulgsumlem2  41969  lincsum  42012  lincsumcl  42014  lincscmcl  42015  isldepslvec2  42068  modn0mul  42109  digexp  42199