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  3483  cgsex4g  3484  cgsex4gOLD  3485  spc2egv  3550  spc2ed  3552  uneqin  4238  2reu4lem  4471  2reu4  4472  disjpr2  4665  ssunieq  4894  iuneq1  4958  iuneq2  4961  copsex2t  5435  propeqop  5450  opthhausdorff  5460  opthhausdorff0  5461  iunopeqop  5464  soeq2  5549  opbrop  5717  xpsspw  5753  coeq1  5801  coeq2  5802  cnveq  5817  dmeq  5847  sotri  6078  tz7.7  6337  funun  6532  fununfun  6534  fundif  6535  funprg  6540  funtp  6543  2elresin  6607  funssxp  6684  fssres  6694  f1cof1  6734  foun  6786  f1un  6788  resdif  6789  f1oco  6791  fvun  6918  elfvmptrab1w  6962  elfvmptrab1  6963  fvn0ssdmfun  7013  dff3  7039  exfo  7044  fprg  7094  ftpg  7095  f1ounsn  7212  weisoeq2  7296  oprabv  7412  ndmovdistr  7541  ndmovord  7542  brrpssg  7664  eldifpw  7707  iunpw  7710  epweon  7714  bropfvvvv  8028  f1o2ndf1  8058  poseq  8094  fvn0elsupp  8116  smores  8278  tz7.49  8370  tz7.49c  8371  oaord  8468  oeeulem  8522  nnaord  8540  brecop  8740  brecop2  8741  eroveu  8742  ecopovtrn  8750  ixpeq2  8841  undifixp  8864  sbthlem8  9014  sbthlem9  9015  unxpdom  9150  isinf  9156  f1opwfi  9247  fiin  9313  en2lp  9503  inf3lem3  9527  brttrcl  9610  tcmin  9636  djuexb  9809  alephfp  10006  kmlem16  10064  endjudisj  10067  cofsmo  10167  fin23lem28  10238  axdc3lem2  10349  ac6c4  10379  brdom3  10426  brdom5  10427  brdom4  10428  canthp1lem2  10551  finngch  10553  ordpipq  10840  adderpq  10854  mulerpq  10855  lterpq  10868  genpn0  10901  genpnnp  10903  addclprlem2  10915  addcmpblnr  10967  addsrpr  10973  mulsrpr  10974  addclsr  10981  addasssr  10986  distrsr  10989  0idsr  10995  1idsr  10996  00sr  10997  mulgt0sr  11003  axaddf  11043  axaddass  11054  axdistr  11056  cnegex  11301  recextlem2  11755  difgtsumgt  12441  zaddcl  12518  qaddcl  12865  qmulcl  12867  qreccl  12869  xmulgt0  13184  xrsupsslem  13208  xrinfmsslem  13209  supxrpnf  13219  iccss  13316  difreicc  13386  fzadd2  13461  fzsubel  13462  ssfzunsnext  13471  difelfznle  13544  2ffzeq  13551  nelfzo  13566  fzonmapblen  13610  ubmelfzo  13632  ubmelm1fzo  13665  elfznelfzo  13675  subfzo0  13694  adddivflid  13724  modaddid  13816  modifeq2int  13842  modaddmodup  13843  addmodlteq  13855  fsuppmapnn0fiub  13900  mulexp  14010  mulexpz  14011  leexp1a  14084  faclbnd  14199  hashunx  14295  hashgt23el  14333  wrdeq  14445  ccatcl  14483  swrdnd  14564  swrdnd0  14567  swrdsbslen  14574  swrdspsleq  14575  pfxccat1  14611  swrdswrdlem  14613  pfxccatin12lem2a  14636  swrdccatin2  14638  pfxccatin12lem2  14640  pfxccatin12  14642  swrdccat  14644  reuccatpfxs1  14656  repswswrd  14693  repswccat  14695  cshwidxn  14718  cshweqdif2  14728  2cshwcshw  14734  cshwcshid  14736  cshwcsh2id  14737  f1oun2prg  14826  s2eq2s1eq  14845  s3eqs2s1eq  14847  s3sndisj  14876  s3iunsndisj  14877  sqabsadd  15191  sqabssub  15192  abs2dif  15242  rexanuz  15255  o1of2  15522  o1rlimmul  15528  fsum2dlem  15679  isumltss  15757  fprodser  15858  fprodeq0  15884  fprod2dlem  15889  dvdscmulr  16197  dvdsmulcr  16198  summodnegmod  16199  difmod0  16200  dvds2ln  16202  dvdsflip  16230  divalglem9  16314  gcdcllem3  16414  gcdaddmlem  16437  sqgcd  16475  lcmcllem  16509  lcmabs  16518  lcmgcdlem  16519  lcmgcd  16520  lcmgcdeq  16525  lcmftp  16549  lcmfunsnlem2lem1  16551  qredeq  16570  cncongr1  16580  cncongr2  16581  isprm7  16621  hashgcdlem  16701  dvdsprmpweqle  16800  difsqpwdvds  16801  prmgaplem4  16968  cshwsidrepsw  17007  setsfun0  17085  setsstruct2  17087  xpsfrnel2  17470  isfunc  17773  tsrss  18497  chnpof1  18538  rabsubmgmd  18614  resmgmhm2  18622  mndpfsupp  18677  ismhm0  18700  mhmismgmhm  18701  mndissubm  18717  resmndismnd  18718  resmhm2  18731  submefmnd  18805  sursubmefmnd  18806  injsubmefmnd  18807  grpissubg  19061  gimco  19182  symg2bas  19307  pgrpsubgsymg  19323  symgextf  19331  fvcosymgeq  19343  gsmsymgreqlem1  19344  symgfixf1  19351  efgrelexlema  19663  gsum2dlem1  19884  gsum2dlem2  19885  dvdsr  20282  isrnghmmul  20362  c0ghm  20381  rhmisrnghm  20400  subrngpropd  20485  subrgpropd  20525  rnghmsubcsetclem2  20549  rngcinv  20554  rhmsubcsetclem2  20578  rhmsubcrngclem2  20584  ringcinv  20588  srhmsubc  20597  islmhm2  20974  psgnghm  21519  psgndiflemB  21539  frlmbas3  21715  frlmphl  21720  islindf4  21777  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  28880  brbtwn2  28885  axcontlem2  28945  uspgredg2v  29204  usgredg2v  29207  usgr2v1e2w  29232  nb3gr2nb  29364  cusgredg  29404  cplgr3v  29415  cusgrop  29418  rusgr1vtx  29569  iswlkg  29594  wlkeq  29614  wlk1walk  29619  uspgr2wlkeq2  29627  uspgr2wlkeqi  29628  cyclnumvtx  29780  crctcshwlkn0lem3  29792  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  wspthneq1eq2  29840  wwlksnextinj  29879  2wlkdlem7  29912  2wlkdlem8  29913  2pthon3v  29923  s3wwlks2on  29936  sps3wwlks2on  29937  elwwlks2  29949  elwspths2spth  29950  rusgrnumwwlks  29957  clwlkclwwlklem2a  29980  clwlkclwwlklem3  29983  clwlkclwwlkf1lem2  29987  clwlkclwwlkf1  29992  clwwlknonex2  30091  3wlkdlem3  30143  uhgr3cyclex  30164  cusconngr  30173  eupth0  30196  frgr3v  30257  1to3vfriswmgr  30262  4cycl2v2nb  30271  frgrnbnb  30275  frgrncvvdeq  30291  frgrwopreglem4a  30292  frgrwopreglem5a  30293  frgrwopreglem4  30297  frgrwopreglem5  30303  frgrhash2wsp  30314  numclwwlk1lem2foa  30336  numclwwlk2  30363  blocni  30787  hvsub4  31019  shscli  31299  shscom  31301  spanunsni  31561  spanpr  31562  5oalem2  31637  5oalem3  31638  5oalem5  31640  3oalem1  31644  hoscl  31727  hoadddi  31785  hoadddir  31786  hosub4  31795  lnophsi  31983  hmops  32002  hmopm  32003  adjadd  32075  leop2  32106  leopadd  32114  leopmuli  32115  pjclem4  32181  pj3si  32189  mdslmd1lem2  32308  mdslmd3i  32314  atomli  32364  atcvatlem  32367  chirredlem3  32374  chirredi  32376  atcvat3i  32378  mdsymlem1  32385  mdsymlem5  32389  cdjreui  32414  cdj3i  32423  addltmulALT  32428  hashxpe  32794  domnmuln0rd  33248  mndpluscn  33960  sxbrsigalem5  34322  probfinmeasbALTV  34463  bnj545  34928  bnj546  34929  bnj557  34934  bnj570  34938  bnj594  34945  bnj1001  34992  bnj1118  35017  txpconn  35297  cvmlift2lem10  35377  gonar  35460  lediv2aALT  35742  altopeq12  36027  altxpsspw  36042  funtransport  36096  neibastop1  36424  filnetlem3  36445  lukshef-ax2  36480  arg-ax  36481  nndivsub  36522  bj-nnftht  36806  bj-nnfan  36813  bj-nnfor  36815  copsex2b  37205  isbasisrelowllem1  37420  isbasisrelowllem2  37421  icoreclin  37422  relowlssretop  37428  rdgeqoa  37435  fvineqsnf1  37475  matunitlindflem1  37677  matunitlindflem2  37678  poimirlem4  37685  poimirlem26  37707  poimirlem29  37710  poimirlem30  37711  heicant  37716  mblfinlem1  37718  ismblfin  37722  itg2addnclem  37732  ftc1anclem6  37759  ftc1anclem7  37760  ftc1anclem8  37761  ftc1anc  37762  prdstotbnd  37855  heibor1lem  37870  isdrngo2  38019  divrngidl  38089  pridlc3  38134  linepsubN  39872  pmapsub  39888  elpaddri  39922  paddasslem14  39953  pmapjoin  39972  dvhfvadd  41211  dvhvaddcomN  41216  bcle2d  42293  imacrhmcl  42633  rimco  42637  rmxynorm  43036  monotoddzzfi  43060  acongtr  43096  mpaaeu  43268  oaltublim  43408  omord2lim  43418  cantnftermord  43438  dflim5  43447  omabs2  43450  tfsconcat0i  43463  ofoafo  43474  naddcnff  43480  oaun3lem1  43492  oaun3lem2  43493  pr2cv  43666  brfvrcld2  43810  rfovcnvf1od  44122  ismnushort  44419  nzin  44436  pm10.14  44477  disjrnmpt2  45310  liminfvalxr  45906  etransclem38  46395  cfsetsnfsetf1  47184  tz6.12-afv2  47365  2elfz2melfz  47443  fz0addge0  47444  2ffzoeq  47452  difltmodne  47467  modn0mul  47482  mod2addne  47489  icceuelpartlem  47560  icceuelpart  47561  ich2exprop  47596  sqrtpwpw2p  47663  fmtnoprmfac1lem  47689  fmtnoprmfac1  47690  lighneallem2  47731  divgcdoddALTV  47807  gbowpos  47884  gbowgt5  47887  gboge9  47889  nnsum3primesgbe  47917  bgoldbtbndlem2  47931  bgoldbtbndlem3  47932  isuspgrim  48021  clnbgrgrimlem  48058  clnbgrgrim  48059  isgrtri  48068  isubgr3stgrlem4  48094  grlimgrtri  48128  grlictr  48140  gpgedgvtx0  48186  gpgedg2iv  48192  gpg5nbgrvtx03star  48205  gpg5nbgr3star  48206  pgnbgreunbgrlem3  48243  pgnbgreunbgrlem6  48249  pgn4cyclex  48251  isupwlkg  48262  rngcinvALTV  48401  ringcinvALTV  48435  srhmsubcALTV  48450  mapprop  48471  zlmodzxzadd  48483  domnmsuppn0  48494  ply1mulgsumlem2  48513  lincsum  48555  lincsumcl  48557  lincscmcl  48558  isldepslvec2  48611  digexp  48733  rrx2pnecoorneor  48841  rrx2pnedifcoorneorr  48843  rrx2xpref1o  48844  ehl2eudis0lt  48852  rrx2linest  48868  line2x  48880  itsclc0yqsollem2  48889  seppsepf  49054  thincn0eu  49557