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  1072  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  spc2egv  3599  spc2ed  3601  uneqin  4289  2reu4lem  4522  2reu4  4523  disjpr2  4713  ssunieq  4943  iuneq1  5008  iuneq2  5011  copsex2t  5497  propeqop  5512  opthhausdorff  5522  opthhausdorff0  5523  iunopeqop  5526  soeq2  5614  opbrop  5783  xpsspw  5819  coeq1  5868  coeq2  5869  cnveq  5884  dmeq  5914  sotri  6147  tz7.7  6410  funun  6612  fununfun  6614  fundif  6615  funprg  6620  funtp  6623  2elresin  6689  funssxp  6764  fssres  6774  f1cof1  6814  foun  6866  f1un  6868  resdif  6869  f1oco  6871  fvun  6999  elfvmptrab1w  7043  elfvmptrab1  7044  fvn0ssdmfun  7094  dff3  7120  exfo  7125  fprg  7175  ftpg  7176  f1ounsn  7292  weisoeq2  7376  oprabv  7493  ndmovdistr  7622  ndmovord  7623  brrpssg  7745  eldifpw  7788  iunpw  7791  epweon  7795  bropfvvvv  8117  f1o2ndf1  8147  poseq  8183  fvn0elsupp  8205  wfrlem5OLD  8353  smores  8392  tz7.49  8485  tz7.49c  8486  oaord  8585  oeeulem  8639  nnaord  8657  brecop  8850  brecop2  8851  eroveu  8852  ecopovtrn  8860  ixpeq2  8951  undifixp  8974  undomOLD  9100  sbthlem8  9130  sbthlem9  9131  unxpdom  9289  isinf  9296  isinfOLD  9297  f1opwfi  9396  fiin  9462  en2lp  9646  inf3lem3  9670  brttrcl  9753  tcmin  9781  djuexb  9949  alephfp  10148  kmlem16  10206  endjudisj  10209  cofsmo  10309  fin23lem28  10380  axdc3lem2  10491  ac6c4  10521  brdom3  10568  brdom5  10569  brdom4  10570  canthp1lem2  10693  finngch  10695  ordpipq  10982  adderpq  10996  mulerpq  10997  lterpq  11010  genpn0  11043  genpnnp  11045  addclprlem2  11057  addcmpblnr  11109  addsrpr  11115  mulsrpr  11116  addclsr  11123  addasssr  11128  distrsr  11131  0idsr  11137  1idsr  11138  00sr  11139  mulgt0sr  11145  axaddf  11185  axaddass  11196  axdistr  11198  cnegex  11442  recextlem2  11894  difgtsumgt  12579  zaddcl  12657  qaddcl  13007  qmulcl  13009  qreccl  13011  xmulgt0  13325  xrsupsslem  13349  xrinfmsslem  13350  supxrpnf  13360  iccss  13455  difreicc  13524  fzadd2  13599  fzsubel  13600  ssfzunsnext  13609  difelfznle  13682  2ffzeq  13689  nelfzo  13704  fzonmapblen  13748  ubmelfzo  13769  ubmelm1fzo  13802  elfznelfzo  13811  subfzo0  13828  adddivflid  13858  modifeq2int  13974  modaddmodup  13975  addmodlteq  13987  fsuppmapnn0fiub  14032  mulexp  14142  mulexpz  14143  leexp1a  14215  faclbnd  14329  hashunx  14425  hashgt23el  14463  wrdeq  14574  ccatcl  14612  swrdnd  14692  swrdnd0  14695  swrdsbslen  14702  swrdspsleq  14703  pfxccat1  14740  swrdswrdlem  14742  pfxccatin12lem2a  14765  swrdccatin2  14767  pfxccatin12lem2  14769  pfxccatin12  14771  swrdccat  14773  reuccatpfxs1  14785  repswswrd  14822  repswccat  14824  cshwidxn  14847  cshweqdif2  14857  2cshwcshw  14864  cshwcshid  14866  cshwcsh2id  14867  f1oun2prg  14956  s2eq2s1eq  14975  s3eqs2s1eq  14977  s3sndisj  15006  s3iunsndisj  15007  sqabsadd  15321  sqabssub  15322  abs2dif  15371  rexanuz  15384  o1of2  15649  o1rlimmul  15655  fsum2dlem  15806  isumltss  15884  fprodser  15985  fprodeq0  16011  fprod2dlem  16016  dvdscmulr  16322  dvdsmulcr  16323  summodnegmod  16324  dvds2ln  16326  dvdsflip  16354  divalglem9  16438  gcdcllem3  16538  gcdaddmlem  16561  sqgcd  16599  lcmcllem  16633  lcmabs  16642  lcmgcdlem  16643  lcmgcd  16644  lcmgcdeq  16649  lcmftp  16673  lcmfunsnlem2lem1  16675  qredeq  16694  cncongr1  16704  cncongr2  16705  isprm7  16745  hashgcdlem  16825  dvdsprmpweqle  16924  difsqpwdvds  16925  prmgaplem4  17092  cshwsidrepsw  17131  setsfun0  17209  setsstruct2  17211  xpsfrnel2  17609  isfunc  17909  tsrss  18634  rabsubmgmd  18717  resmgmhm2  18725  mndpfsupp  18780  ismhm0  18803  mhmismgmhm  18804  mndissubm  18820  resmndismnd  18821  resmhm2  18834  submefmnd  18908  sursubmefmnd  18909  injsubmefmnd  18910  grpissubg  19164  gimco  19286  symg2bas  19410  pgrpsubgsymg  19427  symgextf  19435  fvcosymgeq  19447  gsmsymgreqlem1  19448  symgfixf1  19455  efgrelexlema  19767  gsum2dlem1  19988  gsum2dlem2  19989  dvdsr  20362  isrnghmmul  20442  c0ghm  20461  rhmisrnghm  20480  subrngpropd  20568  subrgpropd  20608  rnghmsubcsetclem2  20632  rngcinv  20637  rhmsubcsetclem2  20661  rhmsubcrngclem2  20667  ringcinv  20671  srhmsubc  20680  islmhm2  21037  psgnghm  21598  psgndiflemB  21618  frlmbas3  21796  frlmphl  21801  islindf4  21858  ressmpladd  22047  ressmplmul  22048  mplind  22094  mpomatmul  22452  mavmul0g  22559  1marepvsma1  22589  mdetdiag  22605  slesolvec  22685  cramerimplem2  22690  cramerimplem3  22691  cramerimp  22692  mat2pmatlin  22741  m2pmfzgsumcl  22754  monmatcollpw  22785  pmatcollpw3lem  22789  pmatcollpwscmatlem1  22795  chpmat1dlem  22841  chfacfisf  22860  chfacfisfcpmat  22861  chfacfpmmulgsum2  22871  tgcl  22976  uncld  23049  innei  23133  cnco  23274  uncmp  23411  txbas  23575  txbasval  23614  tx1stc  23658  fbun  23848  infil  23871  fbunfip  23877  filuni  23893  imaelfm  23959  txflf  24014  tsmsfbas  24136  tsmsxp  24163  blin2  24439  nmhmplusg  24778  qtopbaslem  24779  iccntr  24843  ncvspi  25190  ncvs1  25191  unmbl  25572  volfiniun  25582  mbfi1flimlem  25757  ply1idom  26164  logreclem  26805  relogbcxpb  26830  fsumvma2  27258  chpchtsum  27263  dchrelbas3  27282  dchrmulcl  27293  lgsmulsqcoprm  27387  gausslemma2dlem1a  27409  lgsquad2lem2  27429  dchrisum0fmul  27550  dchrisum0lem1  27560  sltres  27707  nocvxminlem  27822  oldlim  27925  madebdayim  27926  madebdaylemlrcut  27937  readdscl  28431  remulscl  28434  ishpg  28767  brcgr  28915  brbtwn2  28920  axcontlem2  28980  uspgredg2v  29241  usgredg2v  29244  usgr2v1e2w  29269  nb3gr2nb  29401  cusgredg  29441  cplgr3v  29452  cusgrop  29455  rusgr1vtx  29606  iswlkg  29631  wlkeq  29652  wlk1walk  29657  uspgr2wlkeq2  29665  uspgr2wlkeqi  29666  cyclnumvtx  29820  crctcshwlkn0lem3  29832  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  wspthneq1eq2  29880  wwlksnextinj  29919  2wlkdlem7  29952  2wlkdlem8  29953  2pthon3v  29963  s3wwlks2on  29976  elwwlks2  29986  elwspths2spth  29987  rusgrnumwwlks  29994  clwlkclwwlklem2a  30017  clwlkclwwlklem3  30020  clwlkclwwlkf1lem2  30024  clwlkclwwlkf1  30029  clwwlknonex2  30128  3wlkdlem3  30180  uhgr3cyclex  30201  cusconngr  30210  eupth0  30233  frgr3v  30294  1to3vfriswmgr  30299  4cycl2v2nb  30308  frgrnbnb  30312  frgrncvvdeq  30328  frgrwopreglem4a  30329  frgrwopreglem5a  30330  frgrwopreglem4  30334  frgrwopreglem5  30340  frgrhash2wsp  30351  numclwwlk1lem2foa  30373  numclwwlk2  30400  blocni  30824  hvsub4  31056  shscli  31336  shscom  31338  spanunsni  31598  spanpr  31599  5oalem2  31674  5oalem3  31675  5oalem5  31677  3oalem1  31681  hoscl  31764  hoadddi  31822  hoadddir  31823  hosub4  31832  lnophsi  32020  hmops  32039  hmopm  32040  adjadd  32112  leop2  32143  leopadd  32151  leopmuli  32152  pjclem4  32218  pj3si  32226  mdslmd1lem2  32345  mdslmd3i  32351  atomli  32401  atcvatlem  32404  chirredlem3  32411  chirredi  32413  atcvat3i  32415  mdsymlem1  32422  mdsymlem5  32426  cdjreui  32451  cdj3i  32460  addltmulALT  32465  hashxpe  32811  domnmuln0rd  33278  mndpluscn  33925  sxbrsigalem5  34290  probfinmeasbALTV  34431  bnj545  34909  bnj546  34910  bnj557  34915  bnj570  34919  bnj594  34926  bnj1001  34973  bnj1118  34998  txpconn  35237  cvmlift2lem10  35317  gonar  35400  lediv2aALT  35682  altopeq12  35963  altxpsspw  35978  funtransport  36032  neibastop1  36360  filnetlem3  36381  lukshef-ax2  36416  arg-ax  36417  nndivsub  36458  bj-nnftht  36742  bj-nnfan  36749  bj-nnfor  36751  copsex2b  37141  isbasisrelowllem1  37356  isbasisrelowllem2  37357  icoreclin  37358  relowlssretop  37364  rdgeqoa  37371  fvineqsnf1  37411  wl-ax11-lem2  37587  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem4  37631  poimirlem26  37653  poimirlem29  37656  poimirlem30  37657  heicant  37662  mblfinlem1  37664  ismblfin  37668  itg2addnclem  37678  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  prdstotbnd  37801  heibor1lem  37816  isdrngo2  37965  divrngidl  38035  pridlc3  38080  linepsubN  39754  pmapsub  39770  elpaddri  39804  paddasslem14  39835  pmapjoin  39854  dvhfvadd  41093  dvhvaddcomN  41098  bcle2d  42180  imacrhmcl  42524  rimco  42528  rmxynorm  42930  monotoddzzfi  42954  acongtr  42990  mpaaeu  43162  oaltublim  43303  omord2lim  43313  cantnftermord  43333  dflim5  43342  omabs2  43345  tfsconcat0i  43358  ofoafo  43369  naddcnff  43375  oaun3lem1  43387  oaun3lem2  43388  pr2cv  43561  brfvrcld2  43705  rfovcnvf1od  44017  ismnushort  44320  nzin  44337  pm10.14  44378  disjrnmpt2  45193  liminfvalxr  45798  etransclem38  46287  cfsetsnfsetf1  47071  tz6.12-afv2  47252  2elfz2melfz  47330  fz0addge0  47331  2ffzoeq  47339  difltmodne  47344  icceuelpartlem  47422  icceuelpart  47423  ich2exprop  47458  sqrtpwpw2p  47525  fmtnoprmfac1lem  47551  fmtnoprmfac1  47552  lighneallem2  47593  divgcdoddALTV  47669  gbowpos  47746  gbowgt5  47749  gboge9  47751  nnsum3primesgbe  47779  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  clnbgrgrimlem  47901  clnbgrgrim  47902  isgrtri  47910  isubgr3stgrlem4  47936  grlimgrtri  47963  grlictr  47975  gpgedgvtx0  48019  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  isupwlkg  48053  rngcinvALTV  48192  ringcinvALTV  48226  srhmsubcALTV  48241  mapprop  48262  zlmodzxzadd  48274  domnmsuppn0  48285  ply1mulgsumlem2  48304  lincsum  48346  lincsumcl  48348  lincscmcl  48349  isldepslvec2  48402  modn0mul  48441  digexp  48528  rrx2pnecoorneor  48636  rrx2pnedifcoorneorr  48638  rrx2xpref1o  48639  ehl2eudis0lt  48647  rrx2linest  48663  line2x  48675  itsclc0yqsollem2  48684  seppsepf  48826  thincn0eu  49080