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  3506  cgsex4g  3507  cgsex4gOLD  3508  spc2egv  3578  spc2ed  3580  uneqin  4264  2reu4lem  4497  2reu4  4498  disjpr2  4689  ssunieq  4919  iuneq1  4984  iuneq2  4987  copsex2t  5467  propeqop  5482  opthhausdorff  5492  opthhausdorff0  5493  iunopeqop  5496  soeq2  5583  opbrop  5752  xpsspw  5788  coeq1  5837  coeq2  5838  cnveq  5853  dmeq  5883  sotri  6116  tz7.7  6378  funun  6581  fununfun  6583  fundif  6584  funprg  6589  funtp  6592  2elresin  6658  funssxp  6733  fssres  6743  f1cof1  6783  foun  6835  f1un  6837  resdif  6838  f1oco  6840  fvun  6968  elfvmptrab1w  7012  elfvmptrab1  7013  fvn0ssdmfun  7063  dff3  7089  exfo  7094  fprg  7144  ftpg  7145  f1ounsn  7264  weisoeq2  7348  oprabv  7465  ndmovdistr  7594  ndmovord  7595  brrpssg  7717  eldifpw  7760  iunpw  7763  epweon  7767  bropfvvvv  8089  f1o2ndf1  8119  poseq  8155  fvn0elsupp  8177  wfrlem5OLD  8325  smores  8364  tz7.49  8457  tz7.49c  8458  oaord  8557  oeeulem  8611  nnaord  8629  brecop  8822  brecop2  8823  eroveu  8824  ecopovtrn  8832  ixpeq2  8923  undifixp  8946  undomOLD  9072  sbthlem8  9102  sbthlem9  9103  unxpdom  9259  isinf  9266  isinfOLD  9267  f1opwfi  9366  fiin  9432  en2lp  9618  inf3lem3  9642  brttrcl  9725  tcmin  9753  djuexb  9921  alephfp  10120  kmlem16  10178  endjudisj  10181  cofsmo  10281  fin23lem28  10352  axdc3lem2  10463  ac6c4  10493  brdom3  10540  brdom5  10541  brdom4  10542  canthp1lem2  10665  finngch  10667  ordpipq  10954  adderpq  10968  mulerpq  10969  lterpq  10982  genpn0  11015  genpnnp  11017  addclprlem2  11029  addcmpblnr  11081  addsrpr  11087  mulsrpr  11088  addclsr  11095  addasssr  11100  distrsr  11103  0idsr  11109  1idsr  11110  00sr  11111  mulgt0sr  11117  axaddf  11157  axaddass  11168  axdistr  11170  cnegex  11414  recextlem2  11866  difgtsumgt  12552  zaddcl  12630  qaddcl  12979  qmulcl  12981  qreccl  12983  xmulgt0  13297  xrsupsslem  13321  xrinfmsslem  13322  supxrpnf  13332  iccss  13429  difreicc  13499  fzadd2  13574  fzsubel  13575  ssfzunsnext  13584  difelfznle  13657  2ffzeq  13664  nelfzo  13679  fzonmapblen  13723  ubmelfzo  13744  ubmelm1fzo  13777  elfznelfzo  13786  subfzo0  13803  adddivflid  13833  modifeq2int  13949  modaddmodup  13950  addmodlteq  13962  fsuppmapnn0fiub  14007  mulexp  14117  mulexpz  14118  leexp1a  14191  faclbnd  14306  hashunx  14402  hashgt23el  14440  wrdeq  14552  ccatcl  14590  swrdnd  14670  swrdnd0  14673  swrdsbslen  14680  swrdspsleq  14681  pfxccat1  14718  swrdswrdlem  14720  pfxccatin12lem2a  14743  swrdccatin2  14745  pfxccatin12lem2  14747  pfxccatin12  14749  swrdccat  14751  reuccatpfxs1  14763  repswswrd  14800  repswccat  14802  cshwidxn  14825  cshweqdif2  14835  2cshwcshw  14842  cshwcshid  14844  cshwcsh2id  14845  f1oun2prg  14934  s2eq2s1eq  14953  s3eqs2s1eq  14955  s3sndisj  14984  s3iunsndisj  14985  sqabsadd  15299  sqabssub  15300  abs2dif  15349  rexanuz  15362  o1of2  15627  o1rlimmul  15633  fsum2dlem  15784  isumltss  15862  fprodser  15963  fprodeq0  15989  fprod2dlem  15994  dvdscmulr  16302  dvdsmulcr  16303  summodnegmod  16304  dvds2ln  16306  dvdsflip  16334  divalglem9  16418  gcdcllem3  16518  gcdaddmlem  16541  sqgcd  16579  lcmcllem  16613  lcmabs  16622  lcmgcdlem  16623  lcmgcd  16624  lcmgcdeq  16629  lcmftp  16653  lcmfunsnlem2lem1  16655  qredeq  16674  cncongr1  16684  cncongr2  16685  isprm7  16725  hashgcdlem  16805  dvdsprmpweqle  16904  difsqpwdvds  16905  prmgaplem4  17072  cshwsidrepsw  17111  setsfun0  17189  setsstruct2  17191  xpsfrnel2  17576  isfunc  17875  tsrss  18597  rabsubmgmd  18680  resmgmhm2  18688  mndpfsupp  18743  ismhm0  18766  mhmismgmhm  18767  mndissubm  18783  resmndismnd  18784  resmhm2  18797  submefmnd  18871  sursubmefmnd  18872  injsubmefmnd  18873  grpissubg  19127  gimco  19249  symg2bas  19372  pgrpsubgsymg  19388  symgextf  19396  fvcosymgeq  19408  gsmsymgreqlem1  19409  symgfixf1  19416  efgrelexlema  19728  gsum2dlem1  19949  gsum2dlem2  19950  dvdsr  20320  isrnghmmul  20400  c0ghm  20419  rhmisrnghm  20438  subrngpropd  20526  subrgpropd  20566  rnghmsubcsetclem2  20590  rngcinv  20595  rhmsubcsetclem2  20619  rhmsubcrngclem2  20625  ringcinv  20629  srhmsubc  20638  islmhm2  20994  psgnghm  21538  psgndiflemB  21558  frlmbas3  21734  frlmphl  21739  islindf4  21796  ressmpladd  21985  ressmplmul  21986  mplind  22026  mpomatmul  22382  mavmul0g  22489  1marepvsma1  22519  mdetdiag  22535  slesolvec  22615  cramerimplem2  22620  cramerimplem3  22621  cramerimp  22622  mat2pmatlin  22671  m2pmfzgsumcl  22684  monmatcollpw  22715  pmatcollpw3lem  22719  pmatcollpwscmatlem1  22725  chpmat1dlem  22771  chfacfisf  22790  chfacfisfcpmat  22791  chfacfpmmulgsum2  22801  tgcl  22905  uncld  22977  innei  23061  cnco  23202  uncmp  23339  txbas  23503  txbasval  23542  tx1stc  23586  fbun  23776  infil  23799  fbunfip  23805  filuni  23821  imaelfm  23887  txflf  23942  tsmsfbas  24064  tsmsxp  24091  blin2  24366  nmhmplusg  24694  qtopbaslem  24695  iccntr  24759  ncvspi  25106  ncvs1  25107  unmbl  25488  volfiniun  25498  mbfi1flimlem  25673  ply1idom  26080  logreclem  26722  relogbcxpb  26747  fsumvma2  27175  chpchtsum  27180  dchrelbas3  27199  dchrmulcl  27210  lgsmulsqcoprm  27304  gausslemma2dlem1a  27326  lgsquad2lem2  27346  dchrisum0fmul  27467  dchrisum0lem1  27477  sltres  27624  nocvxminlem  27739  oldlim  27842  madebdayim  27843  madebdaylemlrcut  27854  readdscl  28348  remulscl  28351  ishpg  28684  brcgr  28825  brbtwn2  28830  axcontlem2  28890  uspgredg2v  29149  usgredg2v  29152  usgr2v1e2w  29177  nb3gr2nb  29309  cusgredg  29349  cplgr3v  29360  cusgrop  29363  rusgr1vtx  29514  iswlkg  29539  wlkeq  29560  wlk1walk  29565  uspgr2wlkeq2  29573  uspgr2wlkeqi  29574  cyclnumvtx  29728  crctcshwlkn0lem3  29740  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  wspthneq1eq2  29788  wwlksnextinj  29827  2wlkdlem7  29860  2wlkdlem8  29861  2pthon3v  29871  s3wwlks2on  29884  elwwlks2  29894  elwspths2spth  29895  rusgrnumwwlks  29902  clwlkclwwlklem2a  29925  clwlkclwwlklem3  29928  clwlkclwwlkf1lem2  29932  clwlkclwwlkf1  29937  clwwlknonex2  30036  3wlkdlem3  30088  uhgr3cyclex  30109  cusconngr  30118  eupth0  30141  frgr3v  30202  1to3vfriswmgr  30207  4cycl2v2nb  30216  frgrnbnb  30220  frgrncvvdeq  30236  frgrwopreglem4a  30237  frgrwopreglem5a  30238  frgrwopreglem4  30242  frgrwopreglem5  30248  frgrhash2wsp  30259  numclwwlk1lem2foa  30281  numclwwlk2  30308  blocni  30732  hvsub4  30964  shscli  31244  shscom  31246  spanunsni  31506  spanpr  31507  5oalem2  31582  5oalem3  31583  5oalem5  31585  3oalem1  31589  hoscl  31672  hoadddi  31730  hoadddir  31731  hosub4  31740  lnophsi  31928  hmops  31947  hmopm  31948  adjadd  32020  leop2  32051  leopadd  32059  leopmuli  32060  pjclem4  32126  pj3si  32134  mdslmd1lem2  32253  mdslmd3i  32259  atomli  32309  atcvatlem  32312  chirredlem3  32319  chirredi  32321  atcvat3i  32323  mdsymlem1  32330  mdsymlem5  32334  cdjreui  32359  cdj3i  32368  addltmulALT  32373  hashxpe  32732  domnmuln0rd  33215  mndpluscn  33903  sxbrsigalem5  34266  probfinmeasbALTV  34407  bnj545  34872  bnj546  34873  bnj557  34878  bnj570  34882  bnj594  34889  bnj1001  34936  bnj1118  34961  txpconn  35200  cvmlift2lem10  35280  gonar  35363  lediv2aALT  35645  altopeq12  35926  altxpsspw  35941  funtransport  35995  neibastop1  36323  filnetlem3  36344  lukshef-ax2  36379  arg-ax  36380  nndivsub  36421  bj-nnftht  36705  bj-nnfan  36712  bj-nnfor  36714  copsex2b  37104  isbasisrelowllem1  37319  isbasisrelowllem2  37320  icoreclin  37321  relowlssretop  37327  rdgeqoa  37334  fvineqsnf1  37374  wl-ax11-lem2  37550  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem4  37594  poimirlem26  37616  poimirlem29  37619  poimirlem30  37620  heicant  37625  mblfinlem1  37627  ismblfin  37631  itg2addnclem  37641  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  prdstotbnd  37764  heibor1lem  37779  isdrngo2  37928  divrngidl  37998  pridlc3  38043  linepsubN  39717  pmapsub  39733  elpaddri  39767  paddasslem14  39798  pmapjoin  39817  dvhfvadd  41056  dvhvaddcomN  41061  bcle2d  42138  imacrhmcl  42484  rimco  42488  rmxynorm  42889  monotoddzzfi  42913  acongtr  42949  mpaaeu  43121  oaltublim  43261  omord2lim  43271  cantnftermord  43291  dflim5  43300  omabs2  43303  tfsconcat0i  43316  ofoafo  43327  naddcnff  43333  oaun3lem1  43345  oaun3lem2  43346  pr2cv  43519  brfvrcld2  43663  rfovcnvf1od  43975  ismnushort  44273  nzin  44290  pm10.14  44331  disjrnmpt2  45160  liminfvalxr  45760  etransclem38  46249  cfsetsnfsetf1  47036  tz6.12-afv2  47217  2elfz2melfz  47295  fz0addge0  47296  2ffzoeq  47304  difltmodne  47319  icceuelpartlem  47397  icceuelpart  47398  ich2exprop  47433  sqrtpwpw2p  47500  fmtnoprmfac1lem  47526  fmtnoprmfac1  47527  lighneallem2  47568  divgcdoddALTV  47644  gbowpos  47721  gbowgt5  47724  gboge9  47726  nnsum3primesgbe  47754  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  isuspgrim  47857  clnbgrgrimlem  47894  clnbgrgrim  47895  isgrtri  47903  isubgr3stgrlem4  47929  grlimgrtri  47956  grlictr  47968  gpgedgvtx0  48013  gpg5nbgrvtx03star  48030  gpg5nbgr3star  48031  isupwlkg  48060  rngcinvALTV  48199  ringcinvALTV  48233  srhmsubcALTV  48248  mapprop  48269  zlmodzxzadd  48281  domnmsuppn0  48292  ply1mulgsumlem2  48311  lincsum  48353  lincsumcl  48355  lincscmcl  48356  isldepslvec2  48409  modn0mul  48448  digexp  48535  rrx2pnecoorneor  48643  rrx2pnedifcoorneorr  48645  rrx2xpref1o  48646  ehl2eudis0lt  48654  rrx2linest  48670  line2x  48682  itsclc0yqsollem2  48691  seppsepf  48851  thincn0eu  49265