Theorem anim12i 614

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 597	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  615  anim1i  616  anim2i  618  anifp  1072  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spc2egv  3555  spc2ed  3557  uneqin  4243  2reu4lem  4478  2reu4  4479  disjpr2  4672  ssunieq  4901  iuneq1  4965  iuneq2  4968  copsex2t  5448  propeqop  5463  opthhausdorff  5473  opthhausdorff0  5474  iunopeqop  5477  soeq2  5562  opbrop  5730  xpsspw  5766  coeq1  5814  coeq2  5815  cnveq  5830  dmeq  5860  sotri  6092  tz7.7  6351  funun  6546  fununfun  6548  fundif  6549  funprg  6554  funtp  6557  2elresin  6621  funssxp  6698  fssres  6708  f1cof1  6748  foun  6800  f1un  6802  resdif  6803  f1oco  6805  fvun  6932  elfvmptrab1w  6977  elfvmptrab1  6978  fvn0ssdmfun  7028  dff3  7054  exfo  7059  fprg  7110  ftpg  7111  f1ounsn  7228  weisoeq2  7312  oprabv  7428  ndmovdistr  7557  ndmovord  7558  brrpssg  7680  eldifpw  7723  iunpw  7726  epweon  7730  bropfvvvv  8044  f1o2ndf1  8074  poseq  8110  fvn0elsupp  8132  smores  8294  tz7.49  8386  tz7.49c  8387  oaord  8484  oeeulem  8539  nnaord  8557  brecop  8759  brecop2  8760  eroveu  8761  ecopovtrn  8769  ixpeq2  8861  undifixp  8884  sbthlem8  9034  sbthlem9  9035  unxpdom  9171  isinf  9177  f1opwfi  9268  fiin  9337  en2lp  9527  inf3lem3  9551  brttrcl  9634  tcmin  9660  djuexb  9833  alephfp  10030  kmlem16  10088  endjudisj  10091  cofsmo  10191  fin23lem28  10262  axdc3lem2  10373  ac6c4  10403  brdom3  10450  brdom5  10451  brdom4  10452  canthp1lem2  10576  finngch  10578  ordpipq  10865  adderpq  10879  mulerpq  10880  lterpq  10893  genpn0  10926  genpnnp  10928  addclprlem2  10940  addcmpblnr  10992  addsrpr  10998  mulsrpr  10999  addclsr  11006  addasssr  11011  distrsr  11014  0idsr  11020  1idsr  11021  00sr  11022  mulgt0sr  11028  axaddf  11068  axaddass  11079  axdistr  11081  cnegex  11326  recextlem2  11780  difgtsumgt  12466  zaddcl  12543  qaddcl  12890  qmulcl  12892  qreccl  12894  xmulgt0  13210  xrsupsslem  13234  xrinfmsslem  13235  supxrpnf  13245  iccss  13342  difreicc  13412  fzadd2  13487  fzsubel  13488  ssfzunsnext  13497  difelfznle  13570  2ffzeq  13577  nelfzo  13592  fzonmapblen  13636  ubmelfzo  13658  ubmelm1fzo  13691  elfznelfzo  13701  subfzo0  13720  adddivflid  13750  modaddid  13842  modifeq2int  13868  modaddmodup  13869  addmodlteq  13881  fsuppmapnn0fiub  13926  mulexp  14036  mulexpz  14037  leexp1a  14110  faclbnd  14225  hashunx  14321  hashgt23el  14359  wrdeq  14471  ccatcl  14509  swrdnd  14590  swrdnd0  14593  swrdsbslen  14600  swrdspsleq  14601  pfxccat1  14637  swrdswrdlem  14639  pfxccatin12lem2a  14662  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccatin12  14668  swrdccat  14670  reuccatpfxs1  14682  repswswrd  14719  repswccat  14721  cshwidxn  14744  cshweqdif2  14754  2cshwcshw  14760  cshwcshid  14762  cshwcsh2id  14763  f1oun2prg  14852  s2eq2s1eq  14871  s3eqs2s1eq  14873  s3sndisj  14902  s3iunsndisj  14903  sqabsadd  15217  sqabssub  15218  abs2dif  15268  rexanuz  15281  o1of2  15548  o1rlimmul  15554  fsum2dlem  15705  isumltss  15783  fprodser  15884  fprodeq0  15910  fprod2dlem  15915  dvdscmulr  16223  dvdsmulcr  16224  summodnegmod  16225  difmod0  16226  dvds2ln  16228  dvdsflip  16256  divalglem9  16340  gcdcllem3  16440  gcdaddmlem  16463  sqgcd  16501  lcmcllem  16535  lcmabs  16544  lcmgcdlem  16545  lcmgcd  16546  lcmgcdeq  16551  lcmftp  16575  lcmfunsnlem2lem1  16577  qredeq  16596  cncongr1  16606  cncongr2  16607  isprm7  16647  hashgcdlem  16727  dvdsprmpweqle  16826  difsqpwdvds  16827  prmgaplem4  16994  cshwsidrepsw  17033  setsfun0  17111  setsstruct2  17113  xpsfrnel2  17497  isfunc  17800  tsrss  18524  chnpof1  18565  rabsubmgmd  18641  resmgmhm2  18649  mndpfsupp  18704  ismhm0  18727  mhmismgmhm  18728  mndissubm  18744  resmndismnd  18745  resmhm2  18758  submefmnd  18832  sursubmefmnd  18833  injsubmefmnd  18834  grpissubg  19088  gimco  19209  symg2bas  19334  pgrpsubgsymg  19350  symgextf  19358  fvcosymgeq  19370  gsmsymgreqlem1  19371  symgfixf1  19378  efgrelexlema  19690  gsum2dlem1  19911  gsum2dlem2  19912  dvdsr  20310  isrnghmmul  20390  c0ghm  20409  rhmisrnghm  20428  subrngpropd  20513  subrgpropd  20553  rnghmsubcsetclem2  20577  rngcinv  20582  rhmsubcsetclem2  20606  rhmsubcrngclem2  20612  ringcinv  20616  srhmsubc  20625  islmhm2  21002  psgnghm  21547  psgndiflemB  21567  frlmbas3  21743  frlmphl  21748  islindf4  21805  ressmpladd  21996  ressmplmul  21997  mplind  22037  mpomatmul  22402  mavmul0g  22509  1marepvsma1  22539  mdetdiag  22555  slesolvec  22635  cramerimplem2  22640  cramerimplem3  22641  cramerimp  22642  mat2pmatlin  22691  m2pmfzgsumcl  22704  monmatcollpw  22735  pmatcollpw3lem  22739  pmatcollpwscmatlem1  22745  chpmat1dlem  22791  chfacfisf  22810  chfacfisfcpmat  22811  chfacfpmmulgsum2  22821  tgcl  22925  uncld  22997  innei  23081  cnco  23222  uncmp  23359  txbas  23523  txbasval  23562  tx1stc  23606  fbun  23796  infil  23819  fbunfip  23825  filuni  23841  imaelfm  23907  txflf  23962  tsmsfbas  24084  tsmsxp  24111  blin2  24385  nmhmplusg  24713  qtopbaslem  24714  iccntr  24778  ncvspi  25124  ncvs1  25125  unmbl  25506  volfiniun  25516  mbfi1flimlem  25691  ply1idom  26098  logreclem  26740  relogbcxpb  26765  fsumvma2  27193  chpchtsum  27198  dchrelbas3  27217  dchrmulcl  27228  lgsmulsqcoprm  27322  gausslemma2dlem1a  27344  lgsquad2lem2  27364  dchrisum0fmul  27485  dchrisum0lem1  27495  ltsres  27642  nocvxminlem  27762  oldlim  27895  madebdayim  27896  madebdaylemlrcut  27907  readdscl  28507  remulscl  28510  ishpg  28843  brcgr  28985  brbtwn2  28990  axcontlem2  29050  uspgredg2v  29309  usgredg2v  29312  usgr2v1e2w  29337  nb3gr2nb  29469  cusgredg  29509  cplgr3v  29520  cusgrop  29523  rusgr1vtx  29674  iswlkg  29699  wlkeq  29719  wlk1walk  29724  uspgr2wlkeq2  29732  uspgr2wlkeqi  29733  cyclnumvtx  29885  crctcshwlkn0lem3  29897  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  wspthneq1eq2  29945  wwlksnextinj  29984  2wlkdlem7  30017  2wlkdlem8  30018  2pthon3v  30028  s3wwlks2on  30041  sps3wwlks2on  30042  elwwlks2  30054  elwspths2spth  30055  rusgrnumwwlks  30062  clwlkclwwlklem2a  30085  clwlkclwwlklem3  30088  clwlkclwwlkf1lem2  30092  clwlkclwwlkf1  30097  clwwlknonex2  30196  3wlkdlem3  30248  uhgr3cyclex  30269  cusconngr  30278  eupth0  30301  frgr3v  30362  1to3vfriswmgr  30367  4cycl2v2nb  30376  frgrnbnb  30380  frgrncvvdeq  30396  frgrwopreglem4a  30397  frgrwopreglem5a  30398  frgrwopreglem4  30402  frgrwopreglem5  30408  frgrhash2wsp  30419  numclwwlk1lem2foa  30441  numclwwlk2  30468  blocni  30892  hvsub4  31124  shscli  31404  shscom  31406  spanunsni  31666  spanpr  31667  5oalem2  31742  5oalem3  31743  5oalem5  31745  3oalem1  31749  hoscl  31832  hoadddi  31890  hoadddir  31891  hosub4  31900  lnophsi  32088  hmops  32107  hmopm  32108  adjadd  32180  leop2  32211  leopadd  32219  leopmuli  32220  pjclem4  32286  pj3si  32294  mdslmd1lem2  32413  mdslmd3i  32419  atomli  32469  atcvatlem  32472  chirredlem3  32479  chirredi  32481  atcvat3i  32483  mdsymlem1  32490  mdsymlem5  32494  cdjreui  32519  cdj3i  32528  addltmulALT  32533  hashxpe  32897  domnmuln0rd  33367  mndpluscn  34103  sxbrsigalem5  34465  probfinmeasbALTV  34606  bnj545  35070  bnj546  35071  bnj557  35076  bnj570  35080  bnj594  35087  bnj1001  35134  bnj1118  35159  txpconn  35445  cvmlift2lem10  35525  gonar  35608  lediv2aALT  35890  altopeq12  36175  altxpsspw  36190  funtransport  36244  neibastop1  36572  filnetlem3  36593  lukshef-ax2  36628  arg-ax  36629  nndivsub  36670  bj-nnfan  36994  bj-nnfor  36996  cgsex2gd  37389  copsex2b  37392  isbasisrelowllem1  37607  isbasisrelowllem2  37608  icoreclin  37609  relowlssretop  37615  rdgeqoa  37622  fvineqsnf1  37662  matunitlindflem1  37864  matunitlindflem2  37865  poimirlem4  37872  poimirlem26  37894  poimirlem29  37897  poimirlem30  37898  heicant  37903  mblfinlem1  37905  ismblfin  37909  itg2addnclem  37919  ftc1anclem6  37946  ftc1anclem7  37947  ftc1anclem8  37948  ftc1anc  37949  prdstotbnd  38042  heibor1lem  38057  isdrngo2  38206  divrngidl  38276  pridlc3  38321  eldisjdmqsim  39065  linepsubN  40125  pmapsub  40141  elpaddri  40175  paddasslem14  40206  pmapjoin  40225  dvhfvadd  41464  dvhvaddcomN  41469  bcle2d  42546  imacrhmcl  42881  rimco  42885  rmxynorm  43272  monotoddzzfi  43296  acongtr  43332  mpaaeu  43504  oaltublim  43644  omord2lim  43654  cantnftermord  43674  dflim5  43683  omabs2  43686  tfsconcat0i  43699  ofoafo  43710  naddcnff  43716  oaun3lem1  43728  oaun3lem2  43729  pr2cv  43901  brfvrcld2  44045  rfovcnvf1od  44357  ismnushort  44654  nzin  44671  pm10.14  44712  disjrnmpt2  45544  liminfvalxr  46138  etransclem38  46627  cfsetsnfsetf1  47416  tz6.12-afv2  47597  2elfz2melfz  47675  fz0addge0  47676  2ffzoeq  47684  difltmodne  47699  modn0mul  47714  mod2addne  47721  icceuelpartlem  47792  icceuelpart  47793  ich2exprop  47828  sqrtpwpw2p  47895  fmtnoprmfac1lem  47921  fmtnoprmfac1  47922  lighneallem2  47963  divgcdoddALTV  48039  gbowpos  48116  gbowgt5  48119  gboge9  48121  nnsum3primesgbe  48149  bgoldbtbndlem2  48163  bgoldbtbndlem3  48164  isuspgrim  48253  clnbgrgrimlem  48290  clnbgrgrim  48291  isgrtri  48300  isubgr3stgrlem4  48326  grlimgrtri  48360  grlictr  48372  gpgedgvtx0  48418  gpgedg2iv  48424  gpg5nbgrvtx03star  48437  gpg5nbgr3star  48438  pgnbgreunbgrlem3  48475  pgnbgreunbgrlem6  48481  pgn4cyclex  48483  isupwlkg  48494  rngcinvALTV  48633  ringcinvALTV  48667  srhmsubcALTV  48682  mapprop  48703  zlmodzxzadd  48715  domnmsuppn0  48726  ply1mulgsumlem2  48744  lincsum  48786  lincsumcl  48788  lincscmcl  48789  isldepslvec2  48842  digexp  48964  rrx2pnecoorneor  49072  rrx2pnedifcoorneorr  49074  rrx2xpref1o  49075  ehl2eudis0lt  49083  rrx2linest  49099  line2x  49111  itsclc0yqsollem2  49120  seppsepf  49285  thincn0eu  49787