Theorem anim12i 612

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 595	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 206  df-an 396

This theorem is referenced by:  anim12ci  613  anim1i  614  anim2i  616  anifp  1068  norassOLD  1536  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  spc2egv  3528  spc2ed  3530  sseq2  3943  uneqin  4209  2reu4lem  4453  2reu4  4454  disjpr2  4646  ssunieq  4873  iuneq1  4937  iuneq2  4940  copsex2t  5400  propeqop  5415  opthhausdorff  5425  opthhausdorff0  5426  iunopeqop  5429  soeq2  5516  opbrop  5674  xpsspw  5708  coeq1  5755  coeq2  5756  cnveq  5771  dmeq  5801  sotri  6021  tz7.7  6277  funun  6464  fununfun  6466  fundif  6467  funprg  6472  funtp  6475  2elresin  6537  funssxp  6613  fssres  6624  f1cof1  6665  f1coOLD  6667  foun  6718  resdif  6720  f1oco  6722  fvun  6840  elfvmptrab1w  6883  elfvmptrab1  6884  fvn0ssdmfun  6934  dff3  6958  exfo  6963  fprg  7009  ftpg  7010  weisoeq2  7207  oprabv  7313  ndmovdistr  7439  ndmovord  7440  brrpssg  7556  eldifpw  7596  iunpw  7599  bropfvvvv  7903  f1o2ndf1  7934  fvn0elsupp  7967  wfrlem5OLD  8115  smores  8154  tz7.49  8246  tz7.49c  8247  oaord  8340  oeeulem  8394  nnaord  8412  brecop  8557  brecop2  8558  eroveu  8559  ecopovtrn  8567  ixpeq2  8657  undifixp  8680  undom  8800  sbthlem8  8830  sbthlem9  8831  unxpdom  8959  isinf  8965  f1opwfi  9053  fiin  9111  en2lp  9294  inf3lem3  9318  tcmin  9430  djuexb  9598  alephfp  9795  kmlem16  9852  endjudisj  9855  cofsmo  9956  fin23lem28  10027  axdc3lem2  10138  ac6c4  10168  brdom3  10215  brdom5  10216  brdom4  10217  canthp1lem2  10340  finngch  10342  ordpipq  10629  adderpq  10643  mulerpq  10644  lterpq  10657  genpn0  10690  genpnnp  10692  addclprlem2  10704  addcmpblnr  10756  addsrpr  10762  mulsrpr  10763  addclsr  10770  addasssr  10775  distrsr  10778  0idsr  10784  1idsr  10785  00sr  10786  mulgt0sr  10792  axaddf  10832  axaddass  10843  axdistr  10845  cnegex  11086  recextlem2  11536  difgtsumgt  12216  zaddcl  12290  qaddcl  12634  qmulcl  12636  qreccl  12638  xmulgt0  12946  xrsupsslem  12970  xrinfmsslem  12971  supxrpnf  12981  iccss  13076  difreicc  13145  fzadd2  13220  fzsubel  13221  ssfzunsnext  13230  difelfznle  13299  2ffzeq  13306  nelfzo  13321  fzonmapblen  13361  ubmelfzo  13380  ubmelm1fzo  13411  elfznelfzo  13420  subfzo0  13437  adddivflid  13466  modifeq2int  13581  modaddmodup  13582  addmodlteq  13594  fsuppmapnn0fiub  13639  mulexp  13750  mulexpz  13751  leexp1a  13821  faclbnd  13932  hashunx  14029  hashgt23el  14067  wrdeq  14167  ccatcl  14205  swrdnd  14295  swrdnd0  14298  swrdsbslen  14305  swrdspsleq  14306  pfxccat1  14343  swrdswrdlem  14345  pfxccatin12lem2a  14368  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12  14374  swrdccat  14376  reuccatpfxs1  14388  repswswrd  14425  repswccat  14427  cshwidxn  14450  cshweqdif2  14460  2cshwcshw  14466  cshwcshid  14468  cshwcsh2id  14469  f1oun2prg  14558  s2eq2s1eq  14577  s3eqs2s1eq  14579  s3sndisj  14606  s3iunsndisj  14607  sqabsadd  14922  sqabssub  14923  abs2dif  14972  rexanuz  14985  o1of2  15250  o1rlimmul  15256  fsum2dlem  15410  isumltss  15488  fprodser  15587  fprodeq0  15613  fprod2dlem  15618  dvdscmulr  15922  dvdsmulcr  15923  summodnegmod  15924  dvds2ln  15926  dvdsflip  15954  divalglem9  16038  gcdcllem3  16136  gcdaddmlem  16159  gcdabsOLD  16167  sqgcd  16198  lcmcllem  16229  lcmabs  16238  lcmgcdlem  16239  lcmgcd  16240  lcmgcdeq  16245  lcmftp  16269  lcmfunsnlem2lem1  16271  qredeq  16290  cncongr1  16300  cncongr2  16301  isprm7  16341  hashgcdlem  16417  dvdsprmpweqle  16515  difsqpwdvds  16516  prmgaplem4  16683  cshwsidrepsw  16723  setsfun0  16801  setsstruct2  16803  xpsfrnel2  17192  isfunc  17495  tsrss  18222  mndissubm  18361  resmndismnd  18362  resmhm2  18375  submefmnd  18449  sursubmefmnd  18450  injsubmefmnd  18451  grpissubg  18690  gimco  18799  symg2bas  18915  pgrpsubgsymg  18932  symgextf  18940  fvcosymgeq  18952  gsmsymgreqlem1  18953  symgfixf1  18960  efgrelexlema  19270  gsum2dlem1  19486  gsum2dlem2  19487  dvdsr  19803  subrgpropd  19974  islmhm2  20215  psgnghm  20697  psgndiflemB  20717  frlmbas3  20893  frlmphl  20898  islindf4  20955  ressmpladd  21140  ressmplmul  21141  mplind  21188  mpomatmul  21503  mavmul0g  21610  1marepvsma1  21640  mdetdiag  21656  slesolvec  21736  cramerimplem2  21741  cramerimplem3  21742  cramerimp  21743  mat2pmatlin  21792  m2pmfzgsumcl  21805  monmatcollpw  21836  pmatcollpw3lem  21840  pmatcollpwscmatlem1  21846  chpmat1dlem  21892  chfacfisf  21911  chfacfisfcpmat  21912  chfacfpmmulgsum2  21922  tgcl  22027  uncld  22100  innei  22184  cnco  22325  uncmp  22462  txbas  22626  txbasval  22665  tx1stc  22709  fbun  22899  infil  22922  fbunfip  22928  filuni  22944  imaelfm  23010  txflf  23065  tsmsfbas  23187  tsmsxp  23214  blin2  23490  nmhmplusg  23827  qtopbaslem  23828  iccntr  23890  ncvspi  24225  ncvs1  24226  unmbl  24606  volfiniun  24616  mbfi1flimlem  24792  ply1idom  25194  logreclem  25817  relogbcxpb  25842  fsumvma2  26267  chpchtsum  26272  dchrelbas3  26291  dchrmulcl  26302  lgsmulsqcoprm  26396  gausslemma2dlem1a  26418  lgsquad2lem2  26438  dchrisum0fmul  26559  dchrisum0lem1  26569  ishpg  27024  brcgr  27171  brbtwn2  27176  axcontlem2  27236  uspgredg2v  27494  usgredg2v  27497  usgr2v1e2w  27522  nb3gr2nb  27654  cusgredg  27694  cplgr3v  27705  cusgrop  27708  rusgr1vtx  27858  iswlkg  27883  wlkeq  27903  wlk1walk  27908  uspgr2wlkeq2  27916  uspgr2wlkeqi  27917  crctcshwlkn0lem3  28078  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  wspthneq1eq2  28126  wwlksnextinj  28165  2wlkdlem7  28198  2wlkdlem8  28199  2pthon3v  28209  s3wwlks2on  28222  elwwlks2  28232  elwspths2spth  28233  rusgrnumwwlks  28240  clwlkclwwlklem2a  28263  clwlkclwwlklem3  28266  clwlkclwwlkf1lem2  28270  clwlkclwwlkf1  28275  clwwlknonex2  28374  3wlkdlem3  28426  uhgr3cyclex  28447  cusconngr  28456  eupth0  28479  frgr3v  28540  1to3vfriswmgr  28545  4cycl2v2nb  28554  frgrnbnb  28558  frgrncvvdeq  28574  frgrwopreglem4a  28575  frgrwopreglem5a  28576  frgrwopreglem4  28580  frgrwopreglem5  28586  frgrhash2wsp  28597  numclwwlk1lem2foa  28619  numclwwlk2  28646  blocni  29068  hvsub4  29300  shscli  29580  shscom  29582  spanunsni  29842  spanpr  29843  5oalem2  29918  5oalem3  29919  5oalem5  29921  3oalem1  29925  hoscl  30008  hoadddi  30066  hoadddir  30067  hosub4  30076  lnophsi  30264  hmops  30283  hmopm  30284  adjadd  30356  leop2  30387  leopadd  30395  leopmuli  30396  pjclem4  30462  pj3si  30470  mdslmd1lem2  30589  mdslmd3i  30595  atomli  30645  atcvatlem  30648  chirredlem3  30655  chirredi  30657  atcvat3i  30659  mdsymlem1  30666  mdsymlem5  30670  cdjreui  30695  cdj3i  30704  addltmulALT  30709  hashxpe  31029  mndpluscn  31778  sxbrsigalem5  32155  probfinmeasbALTV  32296  bnj545  32775  bnj546  32776  bnj557  32781  bnj570  32785  bnj594  32792  bnj1001  32839  bnj1118  32864  txpconn  33094  cvmlift2lem10  33174  gonar  33257  lediv2aALT  33535  brttrcl  33699  poseq  33729  sltres  33792  nocvxminlem  33899  oldlim  33996  madebdayim  33997  madebdaylemlrcut  34006  altopeq12  34191  altxpsspw  34206  funtransport  34260  neibastop1  34475  filnetlem3  34496  lukshef-ax2  34531  arg-ax  34532  nndivsub  34573  bj-nnftht  34850  bj-nnfan  34857  bj-nnfor  34859  copsex2b  35238  isbasisrelowllem1  35453  isbasisrelowllem2  35454  icoreclin  35455  relowlssretop  35461  rdgeqoa  35468  fvineqsnf1  35508  wl-ax11-lem2  35664  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem4  35708  poimirlem26  35730  poimirlem29  35733  poimirlem30  35734  heicant  35739  mblfinlem1  35741  ismblfin  35745  itg2addnclem  35755  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  prdstotbnd  35879  heibor1lem  35894  isdrngo2  36043  divrngidl  36113  pridlc3  36158  linepsubN  37693  pmapsub  37709  elpaddri  37743  paddasslem14  37774  pmapjoin  37793  dvhfvadd  39032  dvhvaddcomN  39037  andiff  40087  rmxynorm  40656  monotoddzzfi  40680  acongtr  40716  mpaaeu  40891  pr2cv  41044  brfvrcld2  41189  rfovcnvf1od  41501  ismnushort  41808  nzin  41825  pm10.14  41866  disjrnmpt2  42615  liminfvalxr  43214  etransclem38  43703  cfsetsnfsetf1  44440  tz6.12-afv2  44619  2elfz2melfz  44698  fz0addge0  44699  2ffzoeq  44708  icceuelpartlem  44775  icceuelpart  44776  ich2exprop  44811  sqrtpwpw2p  44878  fmtnoprmfac1lem  44904  fmtnoprmfac1  44905  lighneallem2  44946  divgcdoddALTV  45022  gbowpos  45099  gbowgt5  45102  gboge9  45104  nnsum3primesgbe  45132  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  isupwlkg  45187  rabsubmgmd  45233  resmgmhm2  45241  ismhm0  45247  mhmismgmhm  45248  isrnghmmul  45339  c0ghm  45357  rhmisrnghm  45366  rnghmsubcsetclem2  45422  rngcinv  45427  rngcinvALTV  45439  rhmsubcsetclem2  45468  rhmsubcrngclem2  45474  ringcinv  45478  ringcinvALTV  45502  srhmsubc  45522  srhmsubcALTV  45540  mapprop  45570  zlmodzxzadd  45582  domnmsuppn0  45593  mndpfsupp  45600  ply1mulgsumlem2  45616  lincsum  45658  lincsumcl  45660  lincscmcl  45661  isldepslvec2  45714  modn0mul  45754  digexp  45841  rrx2pnecoorneor  45949  rrx2pnedifcoorneorr  45951  rrx2xpref1o  45952  ehl2eudis0lt  45960  rrx2linest  45976  line2x  45988  itsclc0yqsollem2  45997  seppsepf  46110  thincn0eu  46201