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  3482  cgsex4g  3483  cgsex4gOLD  3484  spc2egv  3554  spc2ed  3556  uneqin  4239  2reu4lem  4472  2reu4  4473  disjpr2  4666  ssunieq  4894  iuneq1  4958  iuneq2  4961  copsex2t  5432  propeqop  5447  opthhausdorff  5457  opthhausdorff0  5458  iunopeqop  5461  soeq2  5546  opbrop  5714  xpsspw  5749  coeq1  5797  coeq2  5798  cnveq  5813  dmeq  5843  sotri  6074  tz7.7  6332  funun  6527  fununfun  6529  fundif  6530  funprg  6535  funtp  6538  2elresin  6602  funssxp  6679  fssres  6689  f1cof1  6729  foun  6781  f1un  6783  resdif  6784  f1oco  6786  fvun  6912  elfvmptrab1w  6956  elfvmptrab1  6957  fvn0ssdmfun  7007  dff3  7033  exfo  7038  fprg  7088  ftpg  7089  f1ounsn  7206  weisoeq2  7290  oprabv  7406  ndmovdistr  7535  ndmovord  7536  brrpssg  7658  eldifpw  7701  iunpw  7704  epweon  7708  bropfvvvv  8022  f1o2ndf1  8052  poseq  8088  fvn0elsupp  8110  smores  8272  tz7.49  8364  tz7.49c  8365  oaord  8462  oeeulem  8516  nnaord  8534  brecop  8734  brecop2  8735  eroveu  8736  ecopovtrn  8744  ixpeq2  8835  undifixp  8858  sbthlem8  9007  sbthlem9  9008  unxpdom  9143  isinf  9149  f1opwfi  9240  fiin  9306  en2lp  9496  inf3lem3  9520  brttrcl  9603  tcmin  9629  djuexb  9802  alephfp  9999  kmlem16  10057  endjudisj  10060  cofsmo  10160  fin23lem28  10231  axdc3lem2  10342  ac6c4  10372  brdom3  10419  brdom5  10420  brdom4  10421  canthp1lem2  10544  finngch  10546  ordpipq  10833  adderpq  10847  mulerpq  10848  lterpq  10861  genpn0  10894  genpnnp  10896  addclprlem2  10908  addcmpblnr  10960  addsrpr  10966  mulsrpr  10967  addclsr  10974  addasssr  10979  distrsr  10982  0idsr  10988  1idsr  10989  00sr  10990  mulgt0sr  10996  axaddf  11036  axaddass  11047  axdistr  11049  cnegex  11294  recextlem2  11748  difgtsumgt  12434  zaddcl  12512  qaddcl  12863  qmulcl  12865  qreccl  12867  xmulgt0  13182  xrsupsslem  13206  xrinfmsslem  13207  supxrpnf  13217  iccss  13314  difreicc  13384  fzadd2  13459  fzsubel  13460  ssfzunsnext  13469  difelfznle  13542  2ffzeq  13549  nelfzo  13564  fzonmapblen  13608  ubmelfzo  13630  ubmelm1fzo  13663  elfznelfzo  13673  subfzo0  13692  adddivflid  13722  modaddid  13814  modifeq2int  13840  modaddmodup  13841  addmodlteq  13853  fsuppmapnn0fiub  13898  mulexp  14008  mulexpz  14009  leexp1a  14082  faclbnd  14197  hashunx  14293  hashgt23el  14331  wrdeq  14443  ccatcl  14481  swrdnd  14562  swrdnd0  14565  swrdsbslen  14572  swrdspsleq  14573  pfxccat1  14609  swrdswrdlem  14611  pfxccatin12lem2a  14634  swrdccatin2  14636  pfxccatin12lem2  14638  pfxccatin12  14640  swrdccat  14642  reuccatpfxs1  14654  repswswrd  14691  repswccat  14693  cshwidxn  14716  cshweqdif2  14726  2cshwcshw  14732  cshwcshid  14734  cshwcsh2id  14735  f1oun2prg  14824  s2eq2s1eq  14843  s3eqs2s1eq  14845  s3sndisj  14874  s3iunsndisj  14875  sqabsadd  15189  sqabssub  15190  abs2dif  15240  rexanuz  15253  o1of2  15520  o1rlimmul  15526  fsum2dlem  15677  isumltss  15755  fprodser  15856  fprodeq0  15882  fprod2dlem  15887  dvdscmulr  16195  dvdsmulcr  16196  summodnegmod  16197  difmod0  16198  dvds2ln  16200  dvdsflip  16228  divalglem9  16312  gcdcllem3  16412  gcdaddmlem  16435  sqgcd  16473  lcmcllem  16507  lcmabs  16516  lcmgcdlem  16517  lcmgcd  16518  lcmgcdeq  16523  lcmftp  16547  lcmfunsnlem2lem1  16549  qredeq  16568  cncongr1  16578  cncongr2  16579  isprm7  16619  hashgcdlem  16699  dvdsprmpweqle  16798  difsqpwdvds  16799  prmgaplem4  16966  cshwsidrepsw  17005  setsfun0  17083  setsstruct2  17085  xpsfrnel2  17468  isfunc  17771  tsrss  18495  chnpof1  18536  rabsubmgmd  18612  resmgmhm2  18620  mndpfsupp  18675  ismhm0  18698  mhmismgmhm  18699  mndissubm  18715  resmndismnd  18716  resmhm2  18729  submefmnd  18803  sursubmefmnd  18804  injsubmefmnd  18805  grpissubg  19059  gimco  19181  symg2bas  19306  pgrpsubgsymg  19322  symgextf  19330  fvcosymgeq  19342  gsmsymgreqlem1  19343  symgfixf1  19350  efgrelexlema  19662  gsum2dlem1  19883  gsum2dlem2  19884  dvdsr  20281  isrnghmmul  20361  c0ghm  20380  rhmisrnghm  20399  subrngpropd  20484  subrgpropd  20524  rnghmsubcsetclem2  20548  rngcinv  20553  rhmsubcsetclem2  20577  rhmsubcrngclem2  20583  ringcinv  20587  srhmsubc  20596  islmhm2  20973  psgnghm  21518  psgndiflemB  21538  frlmbas3  21714  frlmphl  21719  islindf4  21776  ressmpladd  21965  ressmplmul  21966  mplind  22006  mpomatmul  22362  mavmul0g  22469  1marepvsma1  22499  mdetdiag  22515  slesolvec  22595  cramerimplem2  22600  cramerimplem3  22601  cramerimp  22602  mat2pmatlin  22651  m2pmfzgsumcl  22664  monmatcollpw  22695  pmatcollpw3lem  22699  pmatcollpwscmatlem1  22705  chpmat1dlem  22751  chfacfisf  22770  chfacfisfcpmat  22771  chfacfpmmulgsum2  22781  tgcl  22885  uncld  22957  innei  23041  cnco  23182  uncmp  23319  txbas  23483  txbasval  23522  tx1stc  23566  fbun  23756  infil  23779  fbunfip  23785  filuni  23801  imaelfm  23867  txflf  23922  tsmsfbas  24044  tsmsxp  24071  blin2  24345  nmhmplusg  24673  qtopbaslem  24674  iccntr  24738  ncvspi  25084  ncvs1  25085  unmbl  25466  volfiniun  25476  mbfi1flimlem  25651  ply1idom  26058  logreclem  26700  relogbcxpb  26725  fsumvma2  27153  chpchtsum  27158  dchrelbas3  27177  dchrmulcl  27188  lgsmulsqcoprm  27282  gausslemma2dlem1a  27304  lgsquad2lem2  27324  dchrisum0fmul  27445  dchrisum0lem1  27455  sltres  27602  nocvxminlem  27718  oldlim  27833  madebdayim  27834  madebdaylemlrcut  27845  readdscl  28402  remulscl  28405  ishpg  28738  brcgr  28879  brbtwn2  28884  axcontlem2  28944  uspgredg2v  29203  usgredg2v  29206  usgr2v1e2w  29231  nb3gr2nb  29363  cusgredg  29403  cplgr3v  29414  cusgrop  29417  rusgr1vtx  29568  iswlkg  29593  wlkeq  29613  wlk1walk  29618  uspgr2wlkeq2  29626  uspgr2wlkeqi  29627  cyclnumvtx  29779  crctcshwlkn0lem3  29791  crctcshwlkn0lem4  29792  crctcshwlkn0lem5  29793  wspthneq1eq2  29839  wwlksnextinj  29878  2wlkdlem7  29911  2wlkdlem8  29912  2pthon3v  29922  s3wwlks2on  29935  elwwlks2  29945  elwspths2spth  29946  rusgrnumwwlks  29953  clwlkclwwlklem2a  29976  clwlkclwwlklem3  29979  clwlkclwwlkf1lem2  29983  clwlkclwwlkf1  29988  clwwlknonex2  30087  3wlkdlem3  30139  uhgr3cyclex  30160  cusconngr  30169  eupth0  30192  frgr3v  30253  1to3vfriswmgr  30258  4cycl2v2nb  30267  frgrnbnb  30271  frgrncvvdeq  30287  frgrwopreglem4a  30288  frgrwopreglem5a  30289  frgrwopreglem4  30293  frgrwopreglem5  30299  frgrhash2wsp  30310  numclwwlk1lem2foa  30332  numclwwlk2  30359  blocni  30783  hvsub4  31015  shscli  31295  shscom  31297  spanunsni  31557  spanpr  31558  5oalem2  31633  5oalem3  31634  5oalem5  31636  3oalem1  31640  hoscl  31723  hoadddi  31781  hoadddir  31782  hosub4  31791  lnophsi  31979  hmops  31998  hmopm  31999  adjadd  32071  leop2  32102  leopadd  32110  leopmuli  32111  pjclem4  32177  pj3si  32185  mdslmd1lem2  32304  mdslmd3i  32310  atomli  32360  atcvatlem  32363  chirredlem3  32370  chirredi  32372  atcvat3i  32374  mdsymlem1  32381  mdsymlem5  32385  cdjreui  32410  cdj3i  32419  addltmulALT  32424  hashxpe  32787  domnmuln0rd  33239  mndpluscn  33937  sxbrsigalem5  34299  probfinmeasbALTV  34440  bnj545  34905  bnj546  34906  bnj557  34911  bnj570  34915  bnj594  34922  bnj1001  34969  bnj1118  34994  txpconn  35274  cvmlift2lem10  35354  gonar  35437  lediv2aALT  35719  altopeq12  36002  altxpsspw  36017  funtransport  36071  neibastop1  36399  filnetlem3  36420  lukshef-ax2  36455  arg-ax  36456  nndivsub  36497  bj-nnftht  36781  bj-nnfan  36788  bj-nnfor  36790  copsex2b  37180  isbasisrelowllem1  37395  isbasisrelowllem2  37396  icoreclin  37397  relowlssretop  37403  rdgeqoa  37410  fvineqsnf1  37450  wl-ax11-lem2  37626  matunitlindflem1  37662  matunitlindflem2  37663  poimirlem4  37670  poimirlem26  37692  poimirlem29  37695  poimirlem30  37696  heicant  37701  mblfinlem1  37703  ismblfin  37707  itg2addnclem  37717  ftc1anclem6  37744  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  prdstotbnd  37840  heibor1lem  37855  isdrngo2  38004  divrngidl  38074  pridlc3  38119  linepsubN  39797  pmapsub  39813  elpaddri  39847  paddasslem14  39878  pmapjoin  39897  dvhfvadd  41136  dvhvaddcomN  41141  bcle2d  42218  imacrhmcl  42553  rimco  42557  rmxynorm  42957  monotoddzzfi  42981  acongtr  43017  mpaaeu  43189  oaltublim  43329  omord2lim  43339  cantnftermord  43359  dflim5  43368  omabs2  43371  tfsconcat0i  43384  ofoafo  43395  naddcnff  43401  oaun3lem1  43413  oaun3lem2  43414  pr2cv  43587  brfvrcld2  43731  rfovcnvf1od  44043  ismnushort  44340  nzin  44357  pm10.14  44398  disjrnmpt2  45231  liminfvalxr  45827  etransclem38  46316  cfsetsnfsetf1  47096  tz6.12-afv2  47277  2elfz2melfz  47355  fz0addge0  47356  2ffzoeq  47364  difltmodne  47379  modn0mul  47394  mod2addne  47401  icceuelpartlem  47472  icceuelpart  47473  ich2exprop  47508  sqrtpwpw2p  47575  fmtnoprmfac1lem  47601  fmtnoprmfac1  47602  lighneallem2  47643  divgcdoddALTV  47719  gbowpos  47796  gbowgt5  47799  gboge9  47801  nnsum3primesgbe  47829  bgoldbtbndlem2  47843  bgoldbtbndlem3  47844  isuspgrim  47933  clnbgrgrimlem  47970  clnbgrgrim  47971  isgrtri  47980  isubgr3stgrlem4  48006  grlimgrtri  48040  grlictr  48052  gpgedgvtx0  48098  gpgedg2iv  48104  gpg5nbgrvtx03star  48117  gpg5nbgr3star  48118  pgnbgreunbgrlem3  48155  pgnbgreunbgrlem6  48161  pgn4cyclex  48163  isupwlkg  48174  rngcinvALTV  48313  ringcinvALTV  48347  srhmsubcALTV  48362  mapprop  48383  zlmodzxzadd  48395  domnmsuppn0  48406  ply1mulgsumlem2  48425  lincsum  48467  lincsumcl  48469  lincscmcl  48470  isldepslvec2  48523  digexp  48645  rrx2pnecoorneor  48753  rrx2pnedifcoorneorr  48755  rrx2xpref1o  48756  ehl2eudis0lt  48764  rrx2linest  48780  line2x  48792  itsclc0yqsollem2  48801  seppsepf  48966  thincn0eu  49469