Theorem anim12i 619

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 602	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anim12ci  620  anim1i  621  anim2i  623  anifp  1077  cgsex2g  3478  cgsex4g  3479  spc2egv  3544  spc2ed  3546  uneqin  4224  2reu4lem  4458  2reu4  4459  disjpr2  4652  ssunieq  4881  iuneq1  4945  iuneq2  4948  copsex2t  5440  propeqop  5455  opthhausdorff  5465  opthhausdorff0  5466  iunopeqop  5469  iunopeqopOLD  5470  soeq2  5555  opbrop  5723  xpsspw  5759  coeq1  5806  coeq2  5807  cnveq  5822  dmeq  5852  sotri  6084  tz7.7  6343  funun  6538  fununfun  6540  fundif  6541  funprg  6546  funtp  6549  2elresin  6613  funssxp  6690  fssres  6700  f1cof1  6740  foun  6792  f1un  6794  resdif  6795  f1oco  6797  fvun  6924  elfvmptrab1w  6970  elfvmptrab1  6971  fvn0ssdmfun  7022  dff3  7048  exfo  7053  fprg  7105  ftpg  7106  f1ounsn  7223  weisoeq2  7307  oprabv  7423  ndmovdistr  7552  ndmovord  7553  brrpssg  7675  eldifpw  7718  iunpw  7721  epweon  7725  bropfvvvv  8038  f1o2ndf1  8068  poseq  8105  fvn0elsupp  8127  smores  8289  tz7.49  8381  tz7.49c  8382  oaord  8479  oeeulem  8534  nnaord  8552  brecop  8754  brecop2  8755  eroveu  8756  ecopovtrn  8764  ixpeq2  8856  undifixp  8879  sbthlem8  9029  sbthlem9  9030  unxpdom  9166  isinf  9172  f1opwfi  9263  fiin  9332  en2lp  9525  inf3lem3  9549  brttrcl  9632  tcmin  9658  djuexb  9831  alephfp  10028  kmlem16  10086  endjudisj  10089  cofsmo  10189  fin23lem28  10260  axdc3lem2  10371  ac6c4  10401  brdom3  10448  brdom5  10449  brdom4  10450  canthp1lem2  10574  finngch  10576  ordpipq  10863  adderpq  10877  mulerpq  10878  lterpq  10891  genpn0  10924  genpnnp  10926  addclprlem2  10938  addcmpblnr  10990  addsrpr  10996  mulsrpr  10997  addclsr  11004  addasssr  11009  distrsr  11012  0idsr  11018  1idsr  11019  00sr  11020  mulgt0sr  11026  axaddf  11066  axaddass  11077  axdistr  11079  cnegex  11325  recextlem2  11779  difgtsumgt  12488  zaddcl  12565  qaddcl  12913  qmulcl  12915  qreccl  12917  xmulgt0  13233  xrsupsslem  13257  xrinfmsslem  13258  supxrpnf  13268  iccss  13365  difreicc  13435  fzadd2  13511  fzsubel  13512  ssfzunsnext  13521  difelfznle  13594  2ffzeq  13601  nelfzo  13617  fzonmapblen  13661  ubmelfzo  13683  ubmelm1fzo  13716  elfznelfzo  13726  subfzo0  13745  adddivflid  13775  modaddid  13867  modifeq2int  13893  modaddmodup  13894  addmodlteq  13906  fsuppmapnn0fiub  13951  mulexp  14061  mulexpz  14062  leexp1a  14135  faclbnd  14250  hashunx  14346  hashgt23el  14384  wrdeq  14496  ccatcl  14534  swrdnd  14615  swrdnd0  14618  swrdsbslen  14625  swrdspsleq  14626  pfxccat1  14662  swrdswrdlem  14664  pfxccatin12lem2a  14687  swrdccatin2  14689  pfxccatin12lem2  14691  pfxccatin12  14693  swrdccat  14695  reuccatpfxs1  14707  repswswrd  14744  repswccat  14746  cshwidxn  14769  cshweqdif2  14779  2cshwcshw  14785  cshwcshid  14787  cshwcsh2id  14788  f1oun2prg  14877  s2eq2s1eq  14896  s3eqs2s1eq  14898  s3sndisj  14927  s3iunsndisj  14928  sqabsadd  15242  sqabssub  15243  abs2dif  15293  rexanuz  15306  o1of2  15573  o1rlimmul  15579  fsum2dlem  15730  isumltss  15811  fprodser  15912  fprodeq0  15938  fprod2dlem  15943  dvdscmulr  16251  dvdsmulcr  16252  summodnegmod  16253  difmod0  16254  dvds2ln  16256  dvdsflip  16284  divalglem9  16368  gcdcllem3  16468  gcdaddmlem  16491  sqgcd  16529  lcmcllem  16563  lcmabs  16572  lcmgcdlem  16573  lcmgcd  16574  lcmgcdeq  16579  lcmftp  16603  lcmfunsnlem2lem1  16605  qredeq  16624  cncongr1  16634  cncongr2  16635  isprm7  16676  hashgcdlem  16756  dvdsprmpweqle  16855  difsqpwdvds  16856  prmgaplem4  17023  cshwsidrepsw  17062  setsfun0  17140  setsstruct2  17142  xpsfrnel2  17526  isfunc  17829  tsrss  18553  chnpof1  18594  rabsubmgmd  18670  resmgmhm2  18678  mndpfsupp  18733  ismhm0  18756  mhmismgmhm  18757  mndissubm  18773  resmndismnd  18774  resmhm2  18787  submefmnd  18861  sursubmefmnd  18862  injsubmefmnd  18863  grpissubg  19120  gimco  19241  symg2bas  19366  pgrpsubgsymg  19382  symgextf  19390  fvcosymgeq  19402  gsmsymgreqlem1  19403  symgfixf1  19410  efgrelexlema  19722  gsum2dlem1  19943  gsum2dlem2  19944  dvdsr  20340  isrnghmmul  20420  c0ghm  20439  rhmisrnghm  20458  subrngpropd  20547  subrgpropd  20587  rnghmsubcsetclem2  20611  rngcinv  20616  rhmsubcsetclem2  20640  rhmsubcrngclem2  20646  ringcinv  20650  srhmsubc  20659  islmhm2  21035  psgnghm  21562  psgndiflemB  21582  frlmbas3  21758  frlmphl  21763  islindf4  21820  ressmpladd  22011  ressmplmul  22012  mplind  22053  mpomatmul  22436  mavmul0g  22543  1marepvsma1  22573  mdetdiag  22589  slesolvec  22669  cramerimplem2  22674  cramerimplem3  22675  cramerimp  22676  mat2pmatlin  22725  m2pmfzgsumcl  22738  monmatcollpw  22769  pmatcollpw3lem  22773  pmatcollpwscmatlem1  22779  chpmat1dlem  22825  chfacfisf  22844  chfacfisfcpmat  22845  chfacfpmmulgsum2  22855  tgcl  22959  uncld  23031  innei  23115  cnco  23256  uncmp  23393  txbas  23557  txbasval  23596  tx1stc  23640  fbun  23830  infil  23853  fbunfip  23859  filuni  23875  imaelfm  23941  txflf  23996  tsmsfbas  24118  tsmsxp  24145  blin2  24419  nmhmplusg  24747  qtopbaslem  24748  iccntr  24812  ncvspi  25148  ncvs1  25149  unmbl  25529  volfiniun  25539  mbfi1flimlem  25714  ply1idom  26115  logreclem  26751  relogbcxpb  26776  fsumvma2  27202  chpchtsum  27207  dchrelbas3  27226  dchrmulcl  27237  lgsmulsqcoprm  27331  gausslemma2dlem1a  27353  lgsquad2lem2  27373  dchrisum0fmul  27494  dchrisum0lem1  27504  ltsres  27651  nocvxminlem  27771  oldlim  27904  madebdayim  27905  madebdaylemlrcut  27916  readdscl  28516  remulscl  28519  ishpg  28852  brcgr  28994  brbtwn2  28999  axcontlem2  29059  uspgredg2v  29318  usgredg2v  29321  usgr2v1e2w  29346  nb3gr2nb  29478  cusgredg  29518  cplgr3v  29529  cusgrop  29532  rusgr1vtx  29682  iswlkg  29707  wlkeq  29727  wlk1walk  29732  uspgr2wlkeq2  29740  uspgr2wlkeqi  29741  cyclnumvtx  29893  crctcshwlkn0lem3  29905  crctcshwlkn0lem4  29906  crctcshwlkn0lem5  29907  wspthneq1eq2  29953  wwlksnextinj  29992  2wlkdlem7  30025  2wlkdlem8  30026  2pthon3v  30036  s3wwlks2on  30049  sps3wwlks2on  30050  elwwlks2  30062  elwspths2spth  30063  rusgrnumwwlks  30070  clwlkclwwlklem2a  30093  clwlkclwwlklem3  30096  clwlkclwwlkf1lem2  30100  clwlkclwwlkf1  30105  clwwlknonex2  30204  3wlkdlem3  30256  uhgr3cyclex  30277  cusconngr  30286  eupth0  30309  frgr3v  30370  1to3vfriswmgr  30375  4cycl2v2nb  30384  frgrnbnb  30388  frgrncvvdeq  30404  frgrwopreglem4a  30405  frgrwopreglem5a  30406  frgrwopreglem4  30410  frgrwopreglem5  30416  frgrhash2wsp  30427  numclwwlk1lem2foa  30449  numclwwlk2  30476  blocni  30901  hvsub4  31133  shscli  31413  shscom  31415  spanunsni  31675  spanpr  31676  5oalem2  31751  5oalem3  31752  5oalem5  31754  3oalem1  31758  hoscl  31841  hoadddi  31899  hoadddir  31900  hosub4  31909  lnophsi  32097  hmops  32116  hmopm  32117  adjadd  32189  leop2  32220  leopadd  32228  leopmuli  32229  pjclem4  32295  pj3si  32303  mdslmd1lem2  32422  mdslmd3i  32428  atomli  32478  atcvatlem  32481  chirredlem3  32488  chirredi  32490  atcvat3i  32492  mdsymlem1  32499  mdsymlem5  32503  cdjreui  32528  cdj3i  32537  addltmulALT  32542  hashxpe  32906  domnmuln0rd  33362  mndpluscn  34117  sxbrsigalem5  34479  probfinmeasbALTV  34620  bnj545  35084  bnj546  35085  bnj557  35090  bnj570  35094  bnj594  35101  bnj1001  35148  bnj1118  35173  txpconn  35467  cvmlift2lem10  35547  gonar  35630  lediv2aALT  35912  altopeq12  36197  altxpsspw  36212  funtransport  36266  neibastop1  36594  filnetlem3  36615  lukshef-ax2  36650  arg-ax  36651  nndivsub  36692  bj-nnfan  37104  bj-nnfor  37106  cgsex2gd  37504  copsex2b  37507  isbasisrelowllem1  37724  isbasisrelowllem2  37725  icoreclin  37726  relowlssretop  37732  rdgeqoa  37739  fvineqsnf1  37779  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem4  37998  poimirlem26  38020  poimirlem29  38023  poimirlem30  38024  heicant  38029  mblfinlem1  38031  ismblfin  38035  itg2addnclem  38045  ftc1anclem6  38072  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  prdstotbnd  38168  heibor1lem  38183  isdrngo2  38332  divrngidl  38402  pridlc3  38447  eldisjdmqsim  39191  linepsubN  40251  pmapsub  40267  elpaddri  40301  paddasslem14  40332  pmapjoin  40351  dvhfvadd  41590  dvhvaddcomN  41595  bcle2d  42671  imacrhmcl  43011  rimco  43012  rmxynorm  43370  monotoddzzfi  43394  acongtr  43430  mpaaeu  43602  oaltublim  43742  omord2lim  43752  cantnftermord  43772  dflim5  43781  omabs2  43784  tfsconcat0i  43797  ofoafo  43808  naddcnff  43814  oaun3lem1  43826  oaun3lem2  43827  pr2cv  43999  brfvrcld2  44143  rfovcnvf1od  44455  ismnushort  44752  nzin  44769  pm10.14  44810  disjrnmpt2  45642  liminfvalxr  46233  etransclem38  46722  cfsetsnfsetf1  47529  tz6.12-afv2  47710  2elfz2melfz  47788  fz0addge0  47789  2ffzoeq  47798  difltmodne  47818  modn0mul  47833  mod2addne  47840  icceuelpartlem  47917  icceuelpart  47918  ich2exprop  47953  sqrtpwpw2p  48023  fmtnoprmfac1lem  48049  fmtnoprmfac1  48050  lighneallem2  48091  divgcdoddALTV  48180  gbowpos  48257  gbowgt5  48260  gboge9  48262  nnsum3primesgbe  48290  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  isuspgrim  48394  clnbgrgrimlem  48431  clnbgrgrim  48432  isgrtri  48441  isubgr3stgrlem4  48467  grlimgrtri  48501  grlictr  48513  gpgedgvtx0  48559  gpgedg2iv  48565  gpg5nbgrvtx03star  48578  gpg5nbgr3star  48579  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem6  48622  pgn4cyclex  48624  isupwlkg  48635  rngcinvALTV  48774  ringcinvALTV  48808  srhmsubcALTV  48823  mapprop  48844  zlmodzxzadd  48856  domnmsuppn0  48867  ply1mulgsumlem2  48885  lincsum  48927  lincsumcl  48929  lincscmcl  48930  isldepslvec2  48983  digexp  49105  rrx2pnecoorneor  49213  rrx2pnedifcoorneorr  49215  rrx2xpref1o  49216  ehl2eudis0lt  49224  rrx2linest  49240  line2x  49252  itsclc0yqsollem2  49261  seppsepf  49426  thincn0eu  49928