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  3484  cgsex4g  3485  cgsex4gOLD  3486  spc2egv  3551  spc2ed  3553  uneqin  4240  2reu4lem  4473  2reu4  4474  disjpr2  4667  ssunieq  4896  iuneq1  4960  iuneq2  4963  copsex2t  5437  propeqop  5452  opthhausdorff  5462  opthhausdorff0  5463  iunopeqop  5466  soeq2  5551  opbrop  5719  xpsspw  5755  coeq1  5804  coeq2  5805  cnveq  5820  dmeq  5850  sotri  6081  tz7.7  6340  funun  6535  fununfun  6537  fundif  6538  funprg  6543  funtp  6546  2elresin  6610  funssxp  6687  fssres  6697  f1cof1  6737  foun  6789  f1un  6791  resdif  6792  f1oco  6794  fvun  6921  elfvmptrab1w  6965  elfvmptrab1  6966  fvn0ssdmfun  7016  dff3  7042  exfo  7047  fprg  7097  ftpg  7098  f1ounsn  7215  weisoeq2  7299  oprabv  7415  ndmovdistr  7544  ndmovord  7545  brrpssg  7667  eldifpw  7710  iunpw  7713  epweon  7717  bropfvvvv  8031  f1o2ndf1  8061  poseq  8097  fvn0elsupp  8119  smores  8281  tz7.49  8373  tz7.49c  8374  oaord  8471  oeeulem  8525  nnaord  8543  brecop  8743  brecop2  8744  eroveu  8745  ecopovtrn  8753  ixpeq2  8844  undifixp  8867  sbthlem8  9017  sbthlem9  9018  unxpdom  9153  isinf  9159  f1opwfi  9250  fiin  9316  en2lp  9506  inf3lem3  9530  brttrcl  9613  tcmin  9639  djuexb  9812  alephfp  10009  kmlem16  10067  endjudisj  10070  cofsmo  10170  fin23lem28  10241  axdc3lem2  10352  ac6c4  10382  brdom3  10429  brdom5  10430  brdom4  10431  canthp1lem2  10554  finngch  10556  ordpipq  10843  adderpq  10857  mulerpq  10858  lterpq  10871  genpn0  10904  genpnnp  10906  addclprlem2  10918  addcmpblnr  10970  addsrpr  10976  mulsrpr  10977  addclsr  10984  addasssr  10989  distrsr  10992  0idsr  10998  1idsr  10999  00sr  11000  mulgt0sr  11006  axaddf  11046  axaddass  11057  axdistr  11059  cnegex  11304  recextlem2  11758  difgtsumgt  12444  zaddcl  12522  qaddcl  12873  qmulcl  12875  qreccl  12877  xmulgt0  13192  xrsupsslem  13216  xrinfmsslem  13217  supxrpnf  13227  iccss  13324  difreicc  13394  fzadd2  13469  fzsubel  13470  ssfzunsnext  13479  difelfznle  13552  2ffzeq  13559  nelfzo  13574  fzonmapblen  13618  ubmelfzo  13640  ubmelm1fzo  13673  elfznelfzo  13683  subfzo0  13702  adddivflid  13732  modaddid  13824  modifeq2int  13850  modaddmodup  13851  addmodlteq  13863  fsuppmapnn0fiub  13908  mulexp  14018  mulexpz  14019  leexp1a  14092  faclbnd  14207  hashunx  14303  hashgt23el  14341  wrdeq  14453  ccatcl  14491  swrdnd  14572  swrdnd0  14575  swrdsbslen  14582  swrdspsleq  14583  pfxccat1  14619  swrdswrdlem  14621  pfxccatin12lem2a  14644  swrdccatin2  14646  pfxccatin12lem2  14648  pfxccatin12  14650  swrdccat  14652  reuccatpfxs1  14664  repswswrd  14701  repswccat  14703  cshwidxn  14726  cshweqdif2  14736  2cshwcshw  14742  cshwcshid  14744  cshwcsh2id  14745  f1oun2prg  14834  s2eq2s1eq  14853  s3eqs2s1eq  14855  s3sndisj  14884  s3iunsndisj  14885  sqabsadd  15199  sqabssub  15200  abs2dif  15250  rexanuz  15263  o1of2  15530  o1rlimmul  15536  fsum2dlem  15687  isumltss  15765  fprodser  15866  fprodeq0  15892  fprod2dlem  15897  dvdscmulr  16205  dvdsmulcr  16206  summodnegmod  16207  difmod0  16208  dvds2ln  16210  dvdsflip  16238  divalglem9  16322  gcdcllem3  16422  gcdaddmlem  16445  sqgcd  16483  lcmcllem  16517  lcmabs  16526  lcmgcdlem  16527  lcmgcd  16528  lcmgcdeq  16533  lcmftp  16557  lcmfunsnlem2lem1  16559  qredeq  16578  cncongr1  16588  cncongr2  16589  isprm7  16629  hashgcdlem  16709  dvdsprmpweqle  16808  difsqpwdvds  16809  prmgaplem4  16976  cshwsidrepsw  17015  setsfun0  17093  setsstruct2  17095  xpsfrnel2  17478  isfunc  17781  tsrss  18505  chnpof1  18546  rabsubmgmd  18622  resmgmhm2  18630  mndpfsupp  18685  ismhm0  18708  mhmismgmhm  18709  mndissubm  18725  resmndismnd  18726  resmhm2  18739  submefmnd  18813  sursubmefmnd  18814  injsubmefmnd  18815  grpissubg  19069  gimco  19190  symg2bas  19315  pgrpsubgsymg  19331  symgextf  19339  fvcosymgeq  19351  gsmsymgreqlem1  19352  symgfixf1  19359  efgrelexlema  19671  gsum2dlem1  19892  gsum2dlem2  19893  dvdsr  20290  isrnghmmul  20370  c0ghm  20389  rhmisrnghm  20408  subrngpropd  20493  subrgpropd  20533  rnghmsubcsetclem2  20557  rngcinv  20562  rhmsubcsetclem2  20586  rhmsubcrngclem2  20592  ringcinv  20596  srhmsubc  20605  islmhm2  20982  psgnghm  21527  psgndiflemB  21547  frlmbas3  21723  frlmphl  21728  islindf4  21785  ressmpladd  21974  ressmplmul  21975  mplind  22015  mpomatmul  22371  mavmul0g  22478  1marepvsma1  22508  mdetdiag  22524  slesolvec  22604  cramerimplem2  22609  cramerimplem3  22610  cramerimp  22611  mat2pmatlin  22660  m2pmfzgsumcl  22673  monmatcollpw  22704  pmatcollpw3lem  22708  pmatcollpwscmatlem1  22714  chpmat1dlem  22760  chfacfisf  22779  chfacfisfcpmat  22780  chfacfpmmulgsum2  22790  tgcl  22894  uncld  22966  innei  23050  cnco  23191  uncmp  23328  txbas  23492  txbasval  23531  tx1stc  23575  fbun  23765  infil  23788  fbunfip  23794  filuni  23810  imaelfm  23876  txflf  23931  tsmsfbas  24053  tsmsxp  24080  blin2  24354  nmhmplusg  24682  qtopbaslem  24683  iccntr  24747  ncvspi  25093  ncvs1  25094  unmbl  25475  volfiniun  25485  mbfi1flimlem  25660  ply1idom  26067  logreclem  26709  relogbcxpb  26734  fsumvma2  27162  chpchtsum  27167  dchrelbas3  27186  dchrmulcl  27197  lgsmulsqcoprm  27291  gausslemma2dlem1a  27313  lgsquad2lem2  27333  dchrisum0fmul  27454  dchrisum0lem1  27464  sltres  27611  nocvxminlem  27727  oldlim  27842  madebdayim  27843  madebdaylemlrcut  27854  readdscl  28411  remulscl  28414  ishpg  28747  brcgr  28889  brbtwn2  28894  axcontlem2  28954  uspgredg2v  29213  usgredg2v  29216  usgr2v1e2w  29241  nb3gr2nb  29373  cusgredg  29413  cplgr3v  29424  cusgrop  29427  rusgr1vtx  29578  iswlkg  29603  wlkeq  29623  wlk1walk  29628  uspgr2wlkeq2  29636  uspgr2wlkeqi  29637  cyclnumvtx  29789  crctcshwlkn0lem3  29801  crctcshwlkn0lem4  29802  crctcshwlkn0lem5  29803  wspthneq1eq2  29849  wwlksnextinj  29888  2wlkdlem7  29921  2wlkdlem8  29922  2pthon3v  29932  s3wwlks2on  29945  sps3wwlks2on  29946  elwwlks2  29958  elwspths2spth  29959  rusgrnumwwlks  29966  clwlkclwwlklem2a  29989  clwlkclwwlklem3  29992  clwlkclwwlkf1lem2  29996  clwlkclwwlkf1  30001  clwwlknonex2  30100  3wlkdlem3  30152  uhgr3cyclex  30173  cusconngr  30182  eupth0  30205  frgr3v  30266  1to3vfriswmgr  30271  4cycl2v2nb  30280  frgrnbnb  30284  frgrncvvdeq  30300  frgrwopreglem4a  30301  frgrwopreglem5a  30302  frgrwopreglem4  30306  frgrwopreglem5  30312  frgrhash2wsp  30323  numclwwlk1lem2foa  30345  numclwwlk2  30372  blocni  30796  hvsub4  31028  shscli  31308  shscom  31310  spanunsni  31570  spanpr  31571  5oalem2  31646  5oalem3  31647  5oalem5  31649  3oalem1  31653  hoscl  31736  hoadddi  31794  hoadddir  31795  hosub4  31804  lnophsi  31992  hmops  32011  hmopm  32012  adjadd  32084  leop2  32115  leopadd  32123  leopmuli  32124  pjclem4  32190  pj3si  32198  mdslmd1lem2  32317  mdslmd3i  32323  atomli  32373  atcvatlem  32376  chirredlem3  32383  chirredi  32385  atcvat3i  32387  mdsymlem1  32394  mdsymlem5  32398  cdjreui  32423  cdj3i  32432  addltmulALT  32437  hashxpe  32800  domnmuln0rd  33252  mndpluscn  33950  sxbrsigalem5  34312  probfinmeasbALTV  34453  bnj545  34918  bnj546  34919  bnj557  34924  bnj570  34928  bnj594  34935  bnj1001  34982  bnj1118  35007  txpconn  35287  cvmlift2lem10  35367  gonar  35450  lediv2aALT  35732  altopeq12  36017  altxpsspw  36032  funtransport  36086  neibastop1  36414  filnetlem3  36435  lukshef-ax2  36470  arg-ax  36471  nndivsub  36512  bj-nnftht  36796  bj-nnfan  36803  bj-nnfor  36805  copsex2b  37195  isbasisrelowllem1  37410  isbasisrelowllem2  37411  icoreclin  37412  relowlssretop  37418  rdgeqoa  37425  fvineqsnf1  37465  matunitlindflem1  37666  matunitlindflem2  37667  poimirlem4  37674  poimirlem26  37696  poimirlem29  37699  poimirlem30  37700  heicant  37705  mblfinlem1  37707  ismblfin  37711  itg2addnclem  37721  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  prdstotbnd  37844  heibor1lem  37859  isdrngo2  38008  divrngidl  38078  pridlc3  38123  linepsubN  39861  pmapsub  39877  elpaddri  39911  paddasslem14  39942  pmapjoin  39961  dvhfvadd  41200  dvhvaddcomN  41205  bcle2d  42282  imacrhmcl  42622  rimco  42626  rmxynorm  43025  monotoddzzfi  43049  acongtr  43085  mpaaeu  43257  oaltublim  43397  omord2lim  43407  cantnftermord  43427  dflim5  43436  omabs2  43439  tfsconcat0i  43452  ofoafo  43463  naddcnff  43469  oaun3lem1  43481  oaun3lem2  43482  pr2cv  43655  brfvrcld2  43799  rfovcnvf1od  44111  ismnushort  44408  nzin  44425  pm10.14  44466  disjrnmpt2  45299  liminfvalxr  45895  etransclem38  46384  cfsetsnfsetf1  47173  tz6.12-afv2  47354  2elfz2melfz  47432  fz0addge0  47433  2ffzoeq  47441  difltmodne  47456  modn0mul  47471  mod2addne  47478  icceuelpartlem  47549  icceuelpart  47550  ich2exprop  47585  sqrtpwpw2p  47652  fmtnoprmfac1lem  47678  fmtnoprmfac1  47679  lighneallem2  47720  divgcdoddALTV  47796  gbowpos  47873  gbowgt5  47876  gboge9  47878  nnsum3primesgbe  47906  bgoldbtbndlem2  47920  bgoldbtbndlem3  47921  isuspgrim  48010  clnbgrgrimlem  48047  clnbgrgrim  48048  isgrtri  48057  isubgr3stgrlem4  48083  grlimgrtri  48117  grlictr  48129  gpgedgvtx0  48175  gpgedg2iv  48181  gpg5nbgrvtx03star  48194  gpg5nbgr3star  48195  pgnbgreunbgrlem3  48232  pgnbgreunbgrlem6  48238  pgn4cyclex  48240  isupwlkg  48251  rngcinvALTV  48390  ringcinvALTV  48424  srhmsubcALTV  48439  mapprop  48460  zlmodzxzadd  48472  domnmsuppn0  48483  ply1mulgsumlem2  48502  lincsum  48544  lincsumcl  48546  lincscmcl  48547  isldepslvec2  48600  digexp  48722  rrx2pnecoorneor  48830  rrx2pnedifcoorneorr  48832  rrx2xpref1o  48833  ehl2eudis0lt  48841  rrx2linest  48857  line2x  48869  itsclc0yqsollem2  48878  seppsepf  49043  thincn0eu  49546