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  3524  cgsex4g  3525  cgsex4gOLD  3526  spc2egv  3598  spc2ed  3600  sseq2  4021  uneqin  4294  2reu4lem  4527  2reu4  4528  disjpr2  4717  ssunieq  4947  iuneq1  5012  iuneq2  5015  copsex2t  5502  propeqop  5516  opthhausdorff  5526  opthhausdorff0  5527  iunopeqop  5530  soeq2  5618  opbrop  5785  xpsspw  5821  coeq1  5870  coeq2  5871  cnveq  5886  dmeq  5916  sotri  6149  tz7.7  6411  funun  6613  fununfun  6615  fundif  6616  funprg  6621  funtp  6624  2elresin  6689  funssxp  6764  fssres  6774  f1cof1  6814  foun  6866  f1un  6868  resdif  6869  f1oco  6871  fvun  6998  elfvmptrab1w  7042  elfvmptrab1  7043  fvn0ssdmfun  7093  dff3  7119  exfo  7124  fprg  7174  ftpg  7175  f1ounsn  7291  weisoeq2  7375  oprabv  7492  ndmovdistr  7621  ndmovord  7622  brrpssg  7743  eldifpw  7786  iunpw  7789  epweon  7793  bropfvvvv  8115  f1o2ndf1  8145  poseq  8181  fvn0elsupp  8203  wfrlem5OLD  8351  smores  8390  tz7.49  8483  tz7.49c  8484  oaord  8583  oeeulem  8637  nnaord  8655  brecop  8848  brecop2  8849  eroveu  8850  ecopovtrn  8858  ixpeq2  8949  undifixp  8972  undomOLD  9098  sbthlem8  9128  sbthlem9  9129  unxpdom  9286  isinf  9293  isinfOLD  9294  f1opwfi  9393  fiin  9459  en2lp  9643  inf3lem3  9667  brttrcl  9750  tcmin  9778  djuexb  9946  alephfp  10145  kmlem16  10203  endjudisj  10206  cofsmo  10306  fin23lem28  10377  axdc3lem2  10488  ac6c4  10518  brdom3  10565  brdom5  10566  brdom4  10567  canthp1lem2  10690  finngch  10692  ordpipq  10979  adderpq  10993  mulerpq  10994  lterpq  11007  genpn0  11040  genpnnp  11042  addclprlem2  11054  addcmpblnr  11106  addsrpr  11112  mulsrpr  11113  addclsr  11120  addasssr  11125  distrsr  11128  0idsr  11134  1idsr  11135  00sr  11136  mulgt0sr  11142  axaddf  11182  axaddass  11193  axdistr  11195  cnegex  11439  recextlem2  11891  difgtsumgt  12576  zaddcl  12654  qaddcl  13004  qmulcl  13006  qreccl  13008  xmulgt0  13321  xrsupsslem  13345  xrinfmsslem  13346  supxrpnf  13356  iccss  13451  difreicc  13520  fzadd2  13595  fzsubel  13596  ssfzunsnext  13605  difelfznle  13678  2ffzeq  13685  nelfzo  13700  fzonmapblen  13744  ubmelfzo  13765  ubmelm1fzo  13798  elfznelfzo  13807  subfzo0  13824  adddivflid  13854  modifeq2int  13970  modaddmodup  13971  addmodlteq  13983  fsuppmapnn0fiub  14028  mulexp  14138  mulexpz  14139  leexp1a  14211  faclbnd  14325  hashunx  14421  hashgt23el  14459  wrdeq  14570  ccatcl  14608  swrdnd  14688  swrdnd0  14691  swrdsbslen  14698  swrdspsleq  14699  pfxccat1  14736  swrdswrdlem  14738  pfxccatin12lem2a  14761  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12  14767  swrdccat  14769  reuccatpfxs1  14781  repswswrd  14818  repswccat  14820  cshwidxn  14843  cshweqdif2  14853  2cshwcshw  14860  cshwcshid  14862  cshwcsh2id  14863  f1oun2prg  14952  s2eq2s1eq  14971  s3eqs2s1eq  14973  s3sndisj  15002  s3iunsndisj  15003  sqabsadd  15317  sqabssub  15318  abs2dif  15367  rexanuz  15380  o1of2  15645  o1rlimmul  15651  fsum2dlem  15802  isumltss  15880  fprodser  15981  fprodeq0  16007  fprod2dlem  16012  dvdscmulr  16318  dvdsmulcr  16319  summodnegmod  16320  dvds2ln  16322  dvdsflip  16350  divalglem9  16434  gcdcllem3  16534  gcdaddmlem  16557  sqgcd  16595  lcmcllem  16629  lcmabs  16638  lcmgcdlem  16639  lcmgcd  16640  lcmgcdeq  16645  lcmftp  16669  lcmfunsnlem2lem1  16671  qredeq  16690  cncongr1  16700  cncongr2  16701  isprm7  16741  hashgcdlem  16821  dvdsprmpweqle  16919  difsqpwdvds  16920  prmgaplem4  17087  cshwsidrepsw  17127  setsfun0  17205  setsstruct2  17207  xpsfrnel2  17610  isfunc  17914  tsrss  18646  rabsubmgmd  18729  resmgmhm2  18737  mndpfsupp  18792  ismhm0  18815  mhmismgmhm  18816  mndissubm  18832  resmndismnd  18833  resmhm2  18846  submefmnd  18920  sursubmefmnd  18921  injsubmefmnd  18922  grpissubg  19176  gimco  19298  symg2bas  19424  pgrpsubgsymg  19441  symgextf  19449  fvcosymgeq  19461  gsmsymgreqlem1  19462  symgfixf1  19469  efgrelexlema  19781  gsum2dlem1  20002  gsum2dlem2  20003  dvdsr  20378  isrnghmmul  20458  c0ghm  20477  rhmisrnghm  20496  subrngpropd  20584  subrgpropd  20624  rnghmsubcsetclem2  20648  rngcinv  20653  rhmsubcsetclem2  20677  rhmsubcrngclem2  20683  ringcinv  20687  srhmsubc  20696  islmhm2  21054  psgnghm  21615  psgndiflemB  21635  frlmbas3  21813  frlmphl  21818  islindf4  21875  ressmpladd  22064  ressmplmul  22065  mplind  22111  mpomatmul  22467  mavmul0g  22574  1marepvsma1  22604  mdetdiag  22620  slesolvec  22700  cramerimplem2  22705  cramerimplem3  22706  cramerimp  22707  mat2pmatlin  22756  m2pmfzgsumcl  22769  monmatcollpw  22800  pmatcollpw3lem  22804  pmatcollpwscmatlem1  22810  chpmat1dlem  22856  chfacfisf  22875  chfacfisfcpmat  22876  chfacfpmmulgsum2  22886  tgcl  22991  uncld  23064  innei  23148  cnco  23289  uncmp  23426  txbas  23590  txbasval  23629  tx1stc  23673  fbun  23863  infil  23886  fbunfip  23892  filuni  23908  imaelfm  23974  txflf  24029  tsmsfbas  24151  tsmsxp  24178  blin2  24454  nmhmplusg  24793  qtopbaslem  24794  iccntr  24856  ncvspi  25203  ncvs1  25204  unmbl  25585  volfiniun  25595  mbfi1flimlem  25771  ply1idom  26178  logreclem  26819  relogbcxpb  26844  fsumvma2  27272  chpchtsum  27277  dchrelbas3  27296  dchrmulcl  27307  lgsmulsqcoprm  27401  gausslemma2dlem1a  27423  lgsquad2lem2  27443  dchrisum0fmul  27564  dchrisum0lem1  27574  sltres  27721  nocvxminlem  27836  oldlim  27939  madebdayim  27940  madebdaylemlrcut  27951  readdscl  28445  remulscl  28448  ishpg  28781  brcgr  28929  brbtwn2  28934  axcontlem2  28994  uspgredg2v  29255  usgredg2v  29258  usgr2v1e2w  29283  nb3gr2nb  29415  cusgredg  29455  cplgr3v  29466  cusgrop  29469  rusgr1vtx  29620  iswlkg  29645  wlkeq  29666  wlk1walk  29671  uspgr2wlkeq2  29679  uspgr2wlkeqi  29680  crctcshwlkn0lem3  29841  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  wspthneq1eq2  29889  wwlksnextinj  29928  2wlkdlem7  29961  2wlkdlem8  29962  2pthon3v  29972  s3wwlks2on  29985  elwwlks2  29995  elwspths2spth  29996  rusgrnumwwlks  30003  clwlkclwwlklem2a  30026  clwlkclwwlklem3  30029  clwlkclwwlkf1lem2  30033  clwlkclwwlkf1  30038  clwwlknonex2  30137  3wlkdlem3  30189  uhgr3cyclex  30210  cusconngr  30219  eupth0  30242  frgr3v  30303  1to3vfriswmgr  30308  4cycl2v2nb  30317  frgrnbnb  30321  frgrncvvdeq  30337  frgrwopreglem4a  30338  frgrwopreglem5a  30339  frgrwopreglem4  30343  frgrwopreglem5  30349  frgrhash2wsp  30360  numclwwlk1lem2foa  30382  numclwwlk2  30409  blocni  30833  hvsub4  31065  shscli  31345  shscom  31347  spanunsni  31607  spanpr  31608  5oalem2  31683  5oalem3  31684  5oalem5  31686  3oalem1  31690  hoscl  31773  hoadddi  31831  hoadddir  31832  hosub4  31841  lnophsi  32029  hmops  32048  hmopm  32049  adjadd  32121  leop2  32152  leopadd  32160  leopmuli  32161  pjclem4  32227  pj3si  32235  mdslmd1lem2  32354  mdslmd3i  32360  atomli  32410  atcvatlem  32413  chirredlem3  32420  chirredi  32422  atcvat3i  32424  mdsymlem1  32431  mdsymlem5  32435  cdjreui  32460  cdj3i  32469  addltmulALT  32474  hashxpe  32816  domnmuln0rd  33260  mndpluscn  33886  sxbrsigalem5  34269  probfinmeasbALTV  34410  bnj545  34887  bnj546  34888  bnj557  34893  bnj570  34897  bnj594  34904  bnj1001  34951  bnj1118  34976  txpconn  35216  cvmlift2lem10  35296  gonar  35379  lediv2aALT  35661  altopeq12  35943  altxpsspw  35958  funtransport  36012  neibastop1  36341  filnetlem3  36362  lukshef-ax2  36397  arg-ax  36398  nndivsub  36439  bj-nnftht  36723  bj-nnfan  36730  bj-nnfor  36732  copsex2b  37122  isbasisrelowllem1  37337  isbasisrelowllem2  37338  icoreclin  37339  relowlssretop  37345  rdgeqoa  37352  fvineqsnf1  37392  wl-ax11-lem2  37566  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem4  37610  poimirlem26  37632  poimirlem29  37635  poimirlem30  37636  heicant  37641  mblfinlem1  37643  ismblfin  37647  itg2addnclem  37657  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  prdstotbnd  37780  heibor1lem  37795  isdrngo2  37944  divrngidl  38014  pridlc3  38059  linepsubN  39734  pmapsub  39750  elpaddri  39784  paddasslem14  39815  pmapjoin  39834  dvhfvadd  41073  dvhvaddcomN  41078  bcle2d  42160  imacrhmcl  42500  rimco  42504  rmxynorm  42906  monotoddzzfi  42930  acongtr  42966  mpaaeu  43138  oaltublim  43279  omord2lim  43289  cantnftermord  43309  dflim5  43318  omabs2  43321  tfsconcat0i  43334  ofoafo  43345  naddcnff  43351  oaun3lem1  43363  oaun3lem2  43364  pr2cv  43537  brfvrcld2  43681  rfovcnvf1od  43993  ismnushort  44296  nzin  44313  pm10.14  44354  disjrnmpt2  45130  liminfvalxr  45738  etransclem38  46227  cfsetsnfsetf1  47008  tz6.12-afv2  47189  2elfz2melfz  47267  fz0addge0  47268  2ffzoeq  47276  difltmodne  47281  icceuelpartlem  47359  icceuelpart  47360  ich2exprop  47395  sqrtpwpw2p  47462  fmtnoprmfac1lem  47488  fmtnoprmfac1  47489  lighneallem2  47530  divgcdoddALTV  47606  gbowpos  47683  gbowgt5  47686  gboge9  47688  nnsum3primesgbe  47716  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  clnbgrgrimlem  47838  clnbgrgrim  47839  isgrtri  47847  isubgr3stgrlem4  47871  grlimgrtri  47898  grlictr  47910  gpgedgvtx0  47953  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  isupwlkg  47980  rngcinvALTV  48119  ringcinvALTV  48153  srhmsubcALTV  48168  mapprop  48190  zlmodzxzadd  48202  domnmsuppn0  48213  ply1mulgsumlem2  48232  lincsum  48274  lincsumcl  48276  lincscmcl  48277  isldepslvec2  48330  modn0mul  48369  digexp  48456  rrx2pnecoorneor  48564  rrx2pnedifcoorneorr  48566  rrx2xpref1o  48567  ehl2eudis0lt  48575  rrx2linest  48591  line2x  48603  itsclc0yqsollem2  48612  seppsepf  48724  thincn0eu  48831