Theorem anim12i 622

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anim12ci  623  anim1i  624  anim2i  626  anifp  1082  cgsex2g  3498  cgsex4g  3499  spc2egv  3557  spc2ed  3559  uneqin  4239  2reu4lem  4474  2reu4  4475  disjpr2  4669  ssunieq  4899  iuneq1  4963  iuneq2  4966  copsex2t  5458  propeqop  5473  opthhausdorff  5483  opthhausdorff0  5484  iunopeqop  5487  iunopeqopOLD  5488  soeq2  5573  opbrop  5741  xpsspw  5778  coeq1  5825  coeq2  5826  cnveq  5841  dmeq  5875  sotri  6109  tz7.7  6366  funun  6561  fununfun  6563  fundif  6564  funprg  6569  funtp  6572  2elresin  6636  funssxp  6714  fssres  6724  f1cof1  6766  foun  6819  f1un  6821  resdif  6822  f1oco  6824  fvun  6951  elfvmptrab1w  6997  elfvmptrab1  6998  fvn0ssdmfun  7049  dff3  7075  exfo  7080  fprg  7132  ftpg  7133  f1ounsn  7250  weisoeq2  7334  oprabv  7450  ndmovdistr  7579  ndmovord  7580  brrpssg  7702  eldifpw  7745  iunpw  7748  epweon  7752  bropfvvvv  8064  f1o2ndf1  8094  poseq  8131  fvn0elsupp  8153  smores  8316  tz7.49  8409  tz7.49c  8410  oaord  8509  oeeulem  8564  nnaord  8582  brecop  8785  brecop2  8786  eroveu  8787  ecopovtrn  8795  ixpeq2  8886  undifixp  8909  sbthlem8  9059  sbthlem9  9060  unxpdom  9196  isinf  9202  f1opwfi  9292  fiin  9361  en2lp  9554  inf3lem3  9578  brttrcl  9661  tcmin  9687  djuexb  9860  alephfp  10057  kmlem16  10115  endjudisj  10118  cofsmo  10219  fin23lem28  10290  axdc3lem2  10401  ac6c4  10431  brdom3  10478  brdom5  10479  brdom4  10480  canthp1lem2  10604  finngch  10606  ordpipq  10893  adderpq  10907  mulerpq  10908  lterpq  10921  genpn0  10954  genpnnp  10956  addclprlem2  10968  addcmpblnr  11020  addsrpr  11026  mulsrpr  11027  addclsr  11034  addasssr  11039  distrsr  11042  0idsr  11048  1idsr  11049  00sr  11050  mulgt0sr  11056  axaddf  11096  axaddass  11107  axdistr  11109  cnegex  11357  recextlem2  11811  difgtsumgt  12527  zaddcl  12604  qaddcl  12959  qmulcl  12961  qreccl  12963  xmulgt0  13279  xrsupsslem  13303  xrinfmsslem  13304  supxrpnf  13314  iccss  13411  difreicc  13481  fzadd2  13557  fzsubel  13558  ssfzunsnext  13567  difelfznle  13640  2ffzeq  13647  nelfzo  13663  fzonmapblen  13707  ubmelfzo  13729  ubmelm1fzo  13762  elfznelfzo  13772  subfzo0  13791  adddivflid  13821  modaddid  13913  modifeq2int  13939  modaddmodup  13940  addmodlteq  13952  fsuppmapnn0fiub  13997  mulexp  14107  mulexpz  14108  leexp1a  14181  faclbnd  14296  hashunx  14392  hashgt23el  14430  wrdeq  14542  ccatcl  14580  swrdnd  14661  swrdnd0  14664  swrdsbslen  14671  swrdspsleq  14672  pfxccat1  14708  swrdswrdlem  14710  pfxccatin12lem2a  14733  swrdccatin2  14735  pfxccatin12lem2  14737  pfxccatin12  14739  swrdccat  14741  reuccatpfxs1  14753  repswswrd  14790  repswccat  14792  cshwidxn  14815  cshweqdif2  14825  2cshwcshw  14831  cshwcshid  14833  cshwcsh2id  14834  f1oun2prg  14923  s2eq2s1eq  14942  s3eqs2s1eq  14944  s3sndisj  14973  s3iunsndisj  14974  sqabsadd  15299  sqabssub  15300  abs2dif  15350  rexanuz  15363  o1of2  15630  o1rlimmul  15636  fsum2dlem  15787  isumltss  15868  fprodser  15969  fprodeq0  15995  fprod2dlem  16000  dvdscmulr  16308  dvdsmulcr  16309  summodnegmod  16310  difmod0  16311  dvds2ln  16313  dvdsflip  16341  divalglem9  16425  gcdcllem3  16525  gcdaddmlem  16548  sqgcd  16586  lcmcllem  16620  lcmabs  16629  lcmgcdlem  16630  lcmgcd  16631  lcmgcdeq  16636  lcmftp  16660  lcmfunsnlem2lem1  16662  qredeq  16681  cncongr1  16691  cncongr2  16692  isprm7  16733  hashgcdlem  16813  dvdsprmpweqle  16912  difsqpwdvds  16913  prmgaplem4  17080  cshwsidrepsw  17119  setsfun0  17198  setsstruct2  17200  xpsfrnel2  17584  isfunc  17887  tsrss  18611  chnpof1  18652  rabsubmgmd  18728  resmgmhm2  18736  mndpfsupp  18791  ismhm0  18814  mhmismgmhm  18815  mndissubm  18831  resmndismnd  18832  resmhm2  18845  submefmnd  18919  sursubmefmnd  18920  injsubmefmnd  18921  grpissubg  19178  gimco  19298  symg2bas  19423  pgrpsubgsymg  19439  symgextf  19447  fvcosymgeq  19459  gsmsymgreqlem1  19460  symgfixf1  19467  efgrelexlema  19779  gsum2dlem1  20000  gsum2dlem2  20001  dvdsr  20397  isrnghmmul  20477  c0ghm  20496  rhmisrnghm  20515  subrngpropd  20604  subrgpropd  20644  rnghmsubcsetclem2  20668  rngcinv  20673  rhmsubcsetclem2  20697  rhmsubcrngclem2  20703  ringcinv  20707  srhmsubc  20716  islmhm2  21092  psgnghm  21619  psgndiflemB  21639  frlmbas3  21815  frlmphl  21820  islindf4  21877  ressmpladd  22068  ressmplmul  22069  mplind  22110  mpomatmul  22493  mavmul0g  22600  1marepvsma1  22630  mdetdiag  22646  slesolvec  22726  cramerimplem2  22731  cramerimplem3  22732  cramerimp  22733  mat2pmatlin  22782  m2pmfzgsumcl  22795  monmatcollpw  22826  pmatcollpw3lem  22830  pmatcollpwscmatlem1  22836  chpmat1dlem  22882  chfacfisf  22901  chfacfisfcpmat  22902  chfacfpmmulgsum2  22912  tgcl  23016  uncld  23088  innei  23172  cnco  23313  uncmp  23450  txbas  23614  txbasval  23653  tx1stc  23697  fbun  23887  infil  23910  fbunfip  23916  filuni  23932  imaelfm  23998  txflf  24053  tsmsfbas  24175  tsmsxp  24202  blin2  24476  nmhmplusg  24804  qtopbaslem  24805  iccntr  24869  ncvspi  25205  ncvs1  25206  unmbl  25586  volfiniun  25596  mbfi1flimlem  25771  ply1idom  26172  logreclem  26814  relogbcxpb  26839  fsumvma2  27265  chpchtsum  27270  dchrelbas3  27289  dchrmulcl  27300  lgsmulsqcoprm  27394  gausslemma2dlem1a  27416  lgsquad2lem2  27436  dchrisum0fmul  27557  dchrisum0lem1  27567  ltsres  27713  nocvxminlem  27834  oldlim  27967  madebdayim  27968  madebdaylemlrcut  27979  readdscl  28579  remulscl  28582  ishpg  28915  brcgr  29057  brbtwn2  29062  axcontlem2  29122  uspgredg2v  29381  usgredg2v  29384  usgr2v1e2w  29409  nb3gr2nb  29541  cusgredg  29581  cplgr3v  29592  cusgrop  29595  rusgr1vtx  29745  iswlkg  29770  wlkeq  29790  wlk1walk  29795  uspgr2wlkeq2  29803  uspgr2wlkeqi  29804  cyclnumvtx  29956  crctcshwlkn0lem3  29968  crctcshwlkn0lem4  29969  crctcshwlkn0lem5  29970  wspthneq1eq2  30016  wwlksnextinj  30055  2wlkdlem7  30088  2wlkdlem8  30089  2pthon3v  30099  s3wwlks2on  30112  sps3wwlks2on  30113  elwwlks2  30125  elwspths2spth  30126  rusgrnumwwlks  30133  clwlkclwwlklem2a  30156  clwlkclwwlklem3  30159  clwlkclwwlkf1lem2  30163  clwlkclwwlkf1  30168  clwwlknonex2  30267  3wlkdlem3  30319  uhgr3cyclex  30340  cusconngr  30349  eupth0  30372  frgr3v  30433  1to3vfriswmgr  30438  4cycl2v2nb  30447  frgrnbnb  30451  frgrncvvdeq  30467  frgrwopreglem4a  30468  frgrwopreglem5a  30469  frgrwopreglem4  30473  frgrwopreglem5  30479  frgrhash2wsp  30490  numclwwlk1lem2foa  30512  numclwwlk2  30539  blocni  30964  hvsub4  31196  shscli  31476  shscom  31478  spanunsni  31738  spanpr  31739  5oalem2  31814  5oalem3  31815  5oalem5  31817  3oalem1  31821  hoscl  31904  hoadddi  31962  hoadddir  31963  hosub4  31972  lnophsi  32160  hmops  32179  hmopm  32180  adjadd  32252  leop2  32283  leopadd  32291  leopmuli  32292  pjclem4  32358  pj3si  32366  mdslmd1lem2  32485  mdslmd3i  32491  atomli  32541  atcvatlem  32544  chirredlem3  32551  chirredi  32553  atcvat3i  32555  mdsymlem1  32562  mdsymlem5  32566  cdjreui  32591  cdj3i  32600  addltmulALT  32605  hashxpe  32969  domnmuln0rd  33418  mndpluscn  34183  sxbrsigalem5  34545  probfinmeasbALTV  34686  bnj545  35150  bnj546  35151  bnj557  35156  bnj570  35160  bnj594  35167  bnj1001  35214  bnj1118  35239  txpconn  35542  cvmlift2lem10  35622  gonar  35705  lediv2aALT  35987  altopeq12  36272  altxpsspw  36287  funtransport  36341  neibastop1  36679  filnetlem3  36700  lukshef-ax2  36735  arg-ax  36736  nndivsub  36777  bj-nnfan  37189  bj-nnfor  37191  cgsex2gd  37589  copsex2b  37592  isbasisrelowllem1  37809  isbasisrelowllem2  37810  icoreclin  37811  relowlssretop  37817  rdgeqoa  37824  fvineqsnf1  37864  matunitlindflem1  38075  matunitlindflem2  38076  poimirlem4  38083  poimirlem26  38105  poimirlem29  38108  poimirlem30  38109  heicant  38114  mblfinlem1  38116  ismblfin  38120  itg2addnclem  38130  ftc1anclem6  38157  ftc1anclem7  38158  ftc1anclem8  38159  ftc1anc  38160  prdstotbnd  38253  heibor1lem  38268  isdrngo2  38417  divrngidl  38487  pridlc3  38532  eldisjdmqsim  39276  linepsubN  40336  pmapsub  40352  elpaddri  40386  paddasslem14  40417  pmapjoin  40436  dvhfvadd  41675  dvhvaddcomN  41680  bcle2d  42756  imacrhmcl  43096  rimco  43097  rmxynorm  43455  monotoddzzfi  43479  acongtr  43515  mpaaeu  43687  oaltublim  43827  omord2lim  43837  cantnftermord  43857  dflim5  43866  omabs2  43869  tfsconcat0i  43882  ofoafo  43893  naddcnff  43899  oaun3lem1  43911  oaun3lem2  43912  pr2cv  44084  brfvrcld2  44228  rfovcnvf1od  44540  ismnushort  44837  nzin  44854  pm10.14  44895  disjrnmpt2  45726  liminfvalxr  46317  etransclem38  46806  cfsetsnfsetf1  47613  tz6.12-afv2  47794  2elfz2melfz  47872  fz0addge0  47873  2ffzoeq  47882  difltmodne  47902  modn0mul  47917  mod2addne  47924  icceuelpartlem  48001  icceuelpart  48002  ich2exprop  48037  sqrtpwpw2p  48107  fmtnoprmfac1lem  48133  fmtnoprmfac1  48134  lighneallem2  48175  divgcdoddALTV  48264  gbowpos  48341  gbowgt5  48344  gboge9  48346  nnsum3primesgbe  48374  bgoldbtbndlem2  48388  bgoldbtbndlem3  48389  isuspgrim  48478  clnbgrgrimlem  48515  clnbgrgrim  48516  isgrtri  48525  isubgr3stgrlem4  48551  grlimgrtri  48585  grlictr  48597  gpgedgvtx0  48643  gpgedg2iv  48649  gpg5nbgrvtx03star  48662  gpg5nbgr3star  48663  pgnbgreunbgrlem3  48700  pgnbgreunbgrlem6  48706  pgn4cyclex  48708  isupwlkg  48719  rngcinvALTV  48858  ringcinvALTV  48892  srhmsubcALTV  48907  mapprop  48928  zlmodzxzadd  48940  domnmsuppn0  48951  ply1mulgsumlem2  48969  lincsum  49011  lincsumcl  49013  lincscmcl  49014  isldepslvec2  49067  digexp  49189  rrx2pnecoorneor  49297  rrx2pnedifcoorneorr  49299  rrx2xpref1o  49300  ehl2eudis0lt  49308  rrx2linest  49324  line2x  49336  itsclc0yqsollem2  49345  seppsepf  49510  thincn0eu  50012