Theorem anim12i 603

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  anim12ci  604  anim1i  605  anim2i  607  anifp  1051  sbimiOLD  2435  sbimiALT  2504  cgsex2g  3459  cgsex4g  3460  spc2egv  3518  spc2ed  3520  sseq2  3883  uneqin  4142  2reu4lem  4348  2reu4  4349  disjpr2  4523  ssunieq  4746  iuneq1  4807  iuneq2  4810  copsex2t  5239  propeqop  5253  opthhausdorff  5263  opthhausdorff0  5264  iunopeqop  5267  soeq2  5347  opbrop  5498  xpsspw  5532  coeq1  5578  coeq2  5579  cnveq  5594  dmeq  5622  sotri  5827  tz7.7  6055  funun  6233  fununfun  6235  fundif  6236  funprg  6241  funtp  6244  2elresin  6301  funssxp  6364  fssres  6373  f1co  6414  foun  6462  resdif  6464  f1oco  6466  fvun  6581  elfvmptrab1  6620  fvn0ssdmfun  6667  dff3  6689  exfo  6694  fprg  6740  ftpg  6741  weisoeq2  6932  oprabv  7033  ndmovdistr  7153  ndmovord  7154  brrpssg  7269  eldifpw  7307  iunpw  7309  bropfvvvv  7595  f1o2ndf1  7623  fvn0elsupp  7649  wfrlem5  7763  smores  7793  tz7.49  7884  tz7.49c  7885  oaord  7974  oeeulem  8028  nnaord  8046  brecop  8190  brecop2  8191  eroveu  8192  ecopovtrn  8200  ixpeq2  8273  undifixp  8295  undom  8401  sbthlem8  8430  sbthlem9  8431  unxpdom  8520  isinf  8526  f1opwfi  8623  fiin  8681  en2lp  8864  inf3lem3  8887  tcmin  8977  djuexb  9132  alephfp  9328  kmlem16  9385  cdaval  9389  endjudisj  9392  cofsmo  9489  fin23lem28  9560  axdc3lem2  9671  ac6c4  9701  brdom3  9748  brdom5  9749  brdom4  9750  canthp1lem2  9873  finngch  9875  ordpipq  10162  adderpq  10176  mulerpq  10177  lterpq  10190  genpn0  10223  genpnnp  10225  addclprlem2  10237  addcmpblnr  10289  addsrpr  10295  mulsrpr  10296  addclsr  10303  addasssr  10308  distrsr  10311  0idsr  10317  1idsr  10318  00sr  10319  mulgt0sr  10325  axaddf  10365  axaddass  10376  axdistr  10378  cnegex  10621  recextlem2  11072  difgtsumgt  11762  zaddcl  11835  qaddcl  12179  qmulcl  12181  qreccl  12183  xmulgt0  12492  xrsupsslem  12516  xrinfmsslem  12517  supxrpnf  12527  iccss  12620  difreicc  12686  fzadd2  12758  fzsubel  12759  ssfzunsnext  12768  difelfznle  12837  2ffzeq  12844  nelfzo  12859  fzonmapblen  12898  ubmelfzo  12917  ubmelm1fzo  12948  elfznelfzo  12957  subfzo0  12974  adddivflid  13003  modifeq2int  13116  modaddmodup  13117  addmodlteq  13129  fsuppmapnn0fiub  13174  mulexp  13283  mulexpz  13284  leexp1a  13354  faclbnd  13465  hashunx  13560  hashgt23el  13598  wrdeq  13697  ccatcl  13737  swrdnd  13822  swrdnd0  13825  swrdeqOLD  13836  swrdsbslen  13841  swrdspsleq  13842  pfxeq  13878  pfxsuffeqwrdeq  13880  pfxccat1  13884  swrdswrdlem  13886  reuccats1OLD  13921  swrdccatin12lem2a  13926  swrdccatin2  13929  pfxccatin12lem2  13931  swrdccatin12lem2OLD  13932  pfxccatin12  13934  swrdccatin12OLD  13935  swrdccat  13938  swrdccatOLD  13939  reuccatpfxs1  13956  repswswrd  14003  repswccat  14005  cshwidxn  14033  cshweqdif2  14043  2cshwcshw  14049  cshwcshid  14051  cshwcsh2id  14052  f1oun2prg  14141  s2eq2s1eq  14160  s3eqs2s1eq  14162  wwlktovf1  14182  s3sndisj  14188  s3iunsndisj  14189  sqabsadd  14503  sqabssub  14504  abs2dif  14553  rexanuz  14566  o1of2  14830  o1rlimmul  14836  fsum2dlem  14985  isumltss  15063  fprodser  15163  fprodeq0  15189  fprod2dlem  15194  dvdscmulr  15498  dvdsmulcr  15499  summodnegmod  15500  dvds2ln  15502  dvdsflip  15527  divalglem9  15612  gcdcllem3  15710  gcdaddmlem  15732  gcdabs  15737  sqgcd  15765  lcmcllem  15796  lcmabs  15805  lcmgcdlem  15806  lcmgcd  15807  lcmgcdeq  15812  lcmftp  15836  lcmfunsnlem2lem1  15838  qredeq  15857  cncongr1  15867  cncongr2  15868  isprm7  15908  hashgcdlem  15981  dvdsprmpweqle  16078  difsqpwdvds  16079  prmgaplem4  16246  cshwsidrepsw  16283  setsfun0  16375  setsstruct2  16377  xpsfrnel2  16694  isfunc  16992  fpwipodrs  17632  tsrss  17691  resmhm2  17828  gimco  18179  symg2bas  18287  pgrpsubgsymg  18297  symgextf  18306  gsmsymgrfixlem1  18316  fvcosymgeq  18318  gsmsymgreqlem1  18319  symgfixf1  18326  efgrelexlema  18635  gsum2dlem1  18843  gsum2dlem2  18844  dvdsr  19119  subrgpropd  19292  islmhm2  19532  ressmpladd  19951  ressmplmul  19952  mplind  19995  psgnghm  20426  psgndiflemB  20446  frlmbas3  20622  frlmphl  20627  islindf4  20684  mpomatmul  20759  mavmul0g  20866  1marepvsma1  20896  mdetdiag  20912  slesolvec  20992  cramerimplem2  20997  cramerimplem3  20998  cramerimp  20999  mat2pmatlin  21047  m2pmfzgsumcl  21060  monmatcollpw  21091  pmatcollpw3lem  21095  pmatcollpwscmatlem1  21101  chpmat1dlem  21147  chfacfisf  21166  chfacfisfcpmat  21167  chfacfpmmulgsum2  21177  tgcl  21281  uncld  21353  innei  21437  cnco  21578  uncmp  21715  txbas  21879  txbasval  21918  tx1stc  21962  fbun  22152  infil  22175  fbunfip  22181  filuni  22197  imaelfm  22263  txflf  22318  tsmsfbas  22439  tsmsxp  22466  blin2  22742  nmhmplusg  23069  qtopbaslem  23070  iccntr  23132  ncvspi  23463  ncvs1  23464  unmbl  23841  volfiniun  23851  mbfi1flimlem  24026  ply1idom  24421  logreclem  25041  relogbcxpb  25066  fsumvma2  25492  chpchtsum  25497  dchrelbas3  25516  dchrmulcl  25527  lgsmulsqcoprm  25621  gausslemma2dlem1a  25643  lgsquad2lem2  25663  dchrisum0fmul  25784  dchrisum0lem1  25794  ishpg  26247  brcgr  26389  brbtwn2  26394  axcontlem2  26454  uspgredg2v  26709  usgredg2v  26712  usgr2v1e2w  26737  nb3gr2nb  26869  cusgredg  26909  cplgr3v  26920  cusgrop  26923  rusgr1vtx  27073  iswlkg  27098  wlkeq  27118  wlk1walk  27123  uspgr2wlkeq2  27131  uspgr2wlkeqi  27132  crctcshwlkn0lem3  27298  crctcshwlkn0lem4  27299  crctcshwlkn0lem5  27300  wspthneq1eq2  27346  wwlksnextinj  27390  wwlksnextinjOLD  27395  2wlkdlem7  27438  2wlkdlem8  27439  2pthon3v  27449  s3wwlks2on  27462  elwwlks2  27472  elwspths2spth  27473  rusgrnumwwlks  27480  rusgrnumwwlksOLD  27481  clwwlkccatlem  27495  clwlkclwwlklem2a  27504  clwlkclwwlklem3  27507  clwlkclwwlkf1lem2  27513  clwlkclwwlkf1lem2OLD  27514  clwlkclwwlkf1OLD  27520  clwlkclwwlkf1  27524  clwwlknonex2  27637  3wlkdlem3  27690  uhgr3cyclex  27711  cusconngr  27720  eupth0  27743  frgr3v  27809  1to3vfriswmgr  27814  4cycl2v2nb  27823  frgrnbnb  27827  frgrncvvdeq  27843  frgrwopreglem4a  27844  frgrwopreglem5a  27845  frgrwopreglem4  27849  frgrwopreglem5  27855  frgrhash2wsp  27866  numclwwlk1lem2foa  27895  numclwwlk1lem2foaOLD  27896  numclwwlk2  27938  blocni  28359  hvsub4  28593  shscli  28875  shscom  28877  spanunsni  29137  spanpr  29138  5oalem2  29213  5oalem3  29214  5oalem5  29216  3oalem1  29220  hoscl  29303  hoadddi  29361  hoadddir  29362  hosub4  29371  lnophsi  29559  hmops  29578  hmopm  29579  adjadd  29651  leop2  29682  leopadd  29690  leopmuli  29691  pjclem4  29757  pj3si  29765  mdslmd1lem2  29884  mdslmd3i  29890  atomli  29940  atcvatlem  29943  chirredlem3  29950  chirredi  29952  atcvat3i  29954  mdsymlem1  29961  mdsymlem5  29965  cdjreui  29990  cdj3i  29999  addltmulALT  30004  hashxpe  30283  mndpluscn  30819  sxbrsigalem5  31197  probfinmeasbOLD  31338  bnj545  31820  bnj546  31821  bnj557  31826  bnj570  31830  bnj594  31837  bnj1001  31883  bnj1118  31907  txpconn  32070  cvmlift2lem10  32150  lediv2aALT  32446  poseq  32622  sltres  32696  nocvxminlem  32774  sslttr  32795  altopeq12  32950  altxpsspw  32965  funtransport  33019  neibastop1  33234  filnetlem3  33255  lukshef-ax2  33289  arg-ax  33290  nndivsub  33331  bj-nnftht  33783  isbasisrelowllem1  34084  isbasisrelowllem2  34085  icoreclin  34086  relowlssretop  34092  rdgeqoa  34099  fvineqsnf1  34138  wl-ax11-lem2  34265  matunitlindflem1  34335  matunitlindflem2  34336  poimirlem4  34343  poimirlem26  34365  poimirlem29  34368  poimirlem30  34369  heicant  34374  mblfinlem1  34376  ismblfin  34380  itg2addnclem  34390  ftc1anclem6  34419  ftc1anclem7  34420  ftc1anclem8  34421  ftc1anc  34422  prdstotbnd  34520  heibor1lem  34535  isdrngo2  34684  divrngidl  34754  pridlc3  34799  linepsubN  36339  pmapsub  36355  elpaddri  36389  paddasslem14  36420  pmapjoin  36439  dvhfvadd  37678  dvhvaddcomN  37683  rmxynorm  38917  monotoddzzfi  38941  acongtr  38977  mpaaeu  39152  brfvrcld2  39406  rfovcnvf1od  39719  nzin  40072  pm10.14  40113  disjrnmpt2  40879  liminfvalxr  41501  etransclem38  41994  tz6.12-afv2  42851  2elfz2melfz  42930  fz0addge0  42931  2ffzoeq  42940  icceuelpartlem  42973  icceuelpart  42974  ich2exprop  43007  sqrtpwpw2p  43074  fmtnoprmfac1lem  43100  fmtnoprmfac1  43101  lighneallem2  43145  divgcdoddALTV  43221  gbowpos  43298  gbowgt5  43301  gboge9  43303  nnsum3primesgbe  43331  bgoldbtbndlem2  43345  bgoldbtbndlem3  43346  isupwlkg  43386  rabsubmgmd  43432  resmgmhm2  43440  ismhm0  43446  mhmismgmhm  43447  isrnghmmul  43534  c0ghm  43552  rhmisrnghm  43561  rnghmsubcsetclem2  43617  rngcinv  43622  rngcinvALTV  43634  rhmsubcsetclem2  43663  rhmsubcrngclem2  43669  ringcinv  43673  ringcinvALTV  43697  srhmsubc  43717  srhmsubcALTV  43735  mapprop  43764  zlmodzxzadd  43776  domnmsuppn0  43789  mndpfsupp  43796  ply1mulgsumlem2  43814  lincsum  43857  lincsumcl  43859  lincscmcl  43860  isldepslvec2  43913  modn0mul  43954  digexp  44041  rrx2pnecoorneor  44076  rrx2pnedifcoorneorr  44078  rrx2xpref1o  44079  ehl2eudis0lt  44087  rrx2linest  44103  line2x  44115  itsclc0yqsollem2  44124