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  3475  cgsex4g  3476  spc2egv  3541  spc2ed  3543  uneqin  4229  2reu4lem  4463  2reu4  4464  disjpr2  4657  ssunieq  4886  iuneq1  4950  iuneq2  4953  copsex2t  5446  propeqop  5461  opthhausdorff  5471  opthhausdorff0  5472  iunopeqop  5475  iunopeqopOLD  5476  soeq2  5561  opbrop  5729  xpsspw  5765  coeq1  5812  coeq2  5813  cnveq  5828  dmeq  5858  sotri  6090  tz7.7  6349  funun  6544  fununfun  6546  fundif  6547  funprg  6552  funtp  6555  2elresin  6619  funssxp  6696  fssres  6706  f1cof1  6746  foun  6798  f1un  6800  resdif  6801  f1oco  6803  fvun  6930  elfvmptrab1w  6975  elfvmptrab1  6976  fvn0ssdmfun  7026  dff3  7052  exfo  7057  fprg  7109  ftpg  7110  f1ounsn  7227  weisoeq2  7311  oprabv  7427  ndmovdistr  7556  ndmovord  7557  brrpssg  7679  eldifpw  7722  iunpw  7725  epweon  7729  bropfvvvv  8042  f1o2ndf1  8072  poseq  8108  fvn0elsupp  8130  smores  8292  tz7.49  8384  tz7.49c  8385  oaord  8482  oeeulem  8537  nnaord  8555  brecop  8757  brecop2  8758  eroveu  8759  ecopovtrn  8767  ixpeq2  8859  undifixp  8882  sbthlem8  9032  sbthlem9  9033  unxpdom  9169  isinf  9175  f1opwfi  9266  fiin  9335  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  11327  recextlem2  11781  difgtsumgt  12490  zaddcl  12567  qaddcl  12915  qmulcl  12917  qreccl  12919  xmulgt0  13235  xrsupsslem  13259  xrinfmsslem  13260  supxrpnf  13270  iccss  13367  difreicc  13437  fzadd2  13513  fzsubel  13514  ssfzunsnext  13523  difelfznle  13596  2ffzeq  13603  nelfzo  13619  fzonmapblen  13663  ubmelfzo  13685  ubmelm1fzo  13718  elfznelfzo  13728  subfzo0  13747  adddivflid  13777  modaddid  13869  modifeq2int  13895  modaddmodup  13896  addmodlteq  13908  fsuppmapnn0fiub  13953  mulexp  14063  mulexpz  14064  leexp1a  14137  faclbnd  14252  hashunx  14348  hashgt23el  14386  wrdeq  14498  ccatcl  14536  swrdnd  14617  swrdnd0  14620  swrdsbslen  14627  swrdspsleq  14628  pfxccat1  14664  swrdswrdlem  14666  pfxccatin12lem2a  14689  swrdccatin2  14691  pfxccatin12lem2  14693  pfxccatin12  14695  swrdccat  14697  reuccatpfxs1  14709  repswswrd  14746  repswccat  14748  cshwidxn  14771  cshweqdif2  14781  2cshwcshw  14787  cshwcshid  14789  cshwcsh2id  14790  f1oun2prg  14879  s2eq2s1eq  14898  s3eqs2s1eq  14900  s3sndisj  14929  s3iunsndisj  14930  sqabsadd  15244  sqabssub  15245  abs2dif  15295  rexanuz  15308  o1of2  15575  o1rlimmul  15581  fsum2dlem  15732  isumltss  15813  fprodser  15914  fprodeq0  15940  fprod2dlem  15945  dvdscmulr  16253  dvdsmulcr  16254  summodnegmod  16255  difmod0  16256  dvds2ln  16258  dvdsflip  16286  divalglem9  16370  gcdcllem3  16470  gcdaddmlem  16493  sqgcd  16531  lcmcllem  16565  lcmabs  16574  lcmgcdlem  16575  lcmgcd  16576  lcmgcdeq  16581  lcmftp  16605  lcmfunsnlem2lem1  16607  qredeq  16626  cncongr1  16636  cncongr2  16637  isprm7  16678  hashgcdlem  16758  dvdsprmpweqle  16857  difsqpwdvds  16858  prmgaplem4  17025  cshwsidrepsw  17064  setsfun0  17142  setsstruct2  17144  xpsfrnel2  17528  isfunc  17831  tsrss  18555  chnpof1  18596  rabsubmgmd  18672  resmgmhm2  18680  mndpfsupp  18735  ismhm0  18758  mhmismgmhm  18759  mndissubm  18775  resmndismnd  18776  resmhm2  18789  submefmnd  18863  sursubmefmnd  18864  injsubmefmnd  18865  grpissubg  19122  gimco  19243  symg2bas  19368  pgrpsubgsymg  19384  symgextf  19392  fvcosymgeq  19404  gsmsymgreqlem1  19405  symgfixf1  19412  efgrelexlema  19724  gsum2dlem1  19945  gsum2dlem2  19946  dvdsr  20342  isrnghmmul  20422  c0ghm  20441  rhmisrnghm  20460  subrngpropd  20545  subrgpropd  20585  rnghmsubcsetclem2  20609  rngcinv  20614  rhmsubcsetclem2  20638  rhmsubcrngclem2  20644  ringcinv  20648  srhmsubc  20657  islmhm2  21033  psgnghm  21560  psgndiflemB  21580  frlmbas3  21756  frlmphl  21761  islindf4  21818  ressmpladd  22007  ressmplmul  22008  mplind  22048  mpomatmul  22411  mavmul0g  22518  1marepvsma1  22548  mdetdiag  22564  slesolvec  22644  cramerimplem2  22649  cramerimplem3  22650  cramerimp  22651  mat2pmatlin  22700  m2pmfzgsumcl  22713  monmatcollpw  22744  pmatcollpw3lem  22748  pmatcollpwscmatlem1  22754  chpmat1dlem  22800  chfacfisf  22819  chfacfisfcpmat  22820  chfacfpmmulgsum2  22830  tgcl  22934  uncld  23006  innei  23090  cnco  23231  uncmp  23368  txbas  23532  txbasval  23571  tx1stc  23615  fbun  23805  infil  23828  fbunfip  23834  filuni  23850  imaelfm  23916  txflf  23971  tsmsfbas  24093  tsmsxp  24120  blin2  24394  nmhmplusg  24722  qtopbaslem  24723  iccntr  24787  ncvspi  25123  ncvs1  25124  unmbl  25504  volfiniun  25514  mbfi1flimlem  25689  ply1idom  26090  logreclem  26726  relogbcxpb  26751  fsumvma2  27177  chpchtsum  27182  dchrelbas3  27201  dchrmulcl  27212  lgsmulsqcoprm  27306  gausslemma2dlem1a  27328  lgsquad2lem2  27348  dchrisum0fmul  27469  dchrisum0lem1  27479  ltsres  27626  nocvxminlem  27746  oldlim  27879  madebdayim  27880  madebdaylemlrcut  27891  readdscl  28491  remulscl  28494  ishpg  28827  brcgr  28969  brbtwn2  28974  axcontlem2  29034  uspgredg2v  29293  usgredg2v  29296  usgr2v1e2w  29321  nb3gr2nb  29453  cusgredg  29493  cplgr3v  29504  cusgrop  29507  rusgr1vtx  29657  iswlkg  29682  wlkeq  29702  wlk1walk  29707  uspgr2wlkeq2  29715  uspgr2wlkeqi  29716  cyclnumvtx  29868  crctcshwlkn0lem3  29880  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  wspthneq1eq2  29928  wwlksnextinj  29967  2wlkdlem7  30000  2wlkdlem8  30001  2pthon3v  30011  s3wwlks2on  30024  sps3wwlks2on  30025  elwwlks2  30037  elwspths2spth  30038  rusgrnumwwlks  30045  clwlkclwwlklem2a  30068  clwlkclwwlklem3  30071  clwlkclwwlkf1lem2  30075  clwlkclwwlkf1  30080  clwwlknonex2  30179  3wlkdlem3  30231  uhgr3cyclex  30252  cusconngr  30261  eupth0  30284  frgr3v  30345  1to3vfriswmgr  30350  4cycl2v2nb  30359  frgrnbnb  30363  frgrncvvdeq  30379  frgrwopreglem4a  30380  frgrwopreglem5a  30381  frgrwopreglem4  30385  frgrwopreglem5  30391  frgrhash2wsp  30402  numclwwlk1lem2foa  30424  numclwwlk2  30451  blocni  30876  hvsub4  31108  shscli  31388  shscom  31390  spanunsni  31650  spanpr  31651  5oalem2  31726  5oalem3  31727  5oalem5  31729  3oalem1  31733  hoscl  31816  hoadddi  31874  hoadddir  31875  hosub4  31884  lnophsi  32072  hmops  32091  hmopm  32092  adjadd  32164  leop2  32195  leopadd  32203  leopmuli  32204  pjclem4  32270  pj3si  32278  mdslmd1lem2  32397  mdslmd3i  32403  atomli  32453  atcvatlem  32456  chirredlem3  32463  chirredi  32465  atcvat3i  32467  mdsymlem1  32474  mdsymlem5  32478  cdjreui  32503  cdj3i  32512  addltmulALT  32517  hashxpe  32880  domnmuln0rd  33335  mndpluscn  34070  sxbrsigalem5  34432  probfinmeasbALTV  34573  bnj545  35037  bnj546  35038  bnj557  35043  bnj570  35047  bnj594  35054  bnj1001  35101  bnj1118  35126  txpconn  35414  cvmlift2lem10  35494  gonar  35577  lediv2aALT  35859  altopeq12  36144  altxpsspw  36159  funtransport  36213  neibastop1  36541  filnetlem3  36562  lukshef-ax2  36597  arg-ax  36598  nndivsub  36639  bj-nnfan  37051  bj-nnfor  37053  cgsex2gd  37451  copsex2b  37454  isbasisrelowllem1  37671  isbasisrelowllem2  37672  icoreclin  37673  relowlssretop  37679  rdgeqoa  37686  fvineqsnf1  37726  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem4  37945  poimirlem26  37967  poimirlem29  37970  poimirlem30  37971  heicant  37976  mblfinlem1  37978  ismblfin  37982  itg2addnclem  37992  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  prdstotbnd  38115  heibor1lem  38130  isdrngo2  38279  divrngidl  38349  pridlc3  38394  eldisjdmqsim  39138  linepsubN  40198  pmapsub  40214  elpaddri  40248  paddasslem14  40279  pmapjoin  40298  dvhfvadd  41537  dvhvaddcomN  41542  bcle2d  42618  imacrhmcl  42959  rimco  42963  rmxynorm  43346  monotoddzzfi  43370  acongtr  43406  mpaaeu  43578  oaltublim  43718  omord2lim  43728  cantnftermord  43748  dflim5  43757  omabs2  43760  tfsconcat0i  43773  ofoafo  43784  naddcnff  43790  oaun3lem1  43802  oaun3lem2  43803  pr2cv  43975  brfvrcld2  44119  rfovcnvf1od  44431  ismnushort  44728  nzin  44745  pm10.14  44786  disjrnmpt2  45618  liminfvalxr  46211  etransclem38  46700  cfsetsnfsetf1  47507  tz6.12-afv2  47688  2elfz2melfz  47766  fz0addge0  47767  2ffzoeq  47776  difltmodne  47796  modn0mul  47811  mod2addne  47818  icceuelpartlem  47895  icceuelpart  47896  ich2exprop  47931  sqrtpwpw2p  48001  fmtnoprmfac1lem  48027  fmtnoprmfac1  48028  lighneallem2  48069  divgcdoddALTV  48158  gbowpos  48235  gbowgt5  48238  gboge9  48240  nnsum3primesgbe  48268  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  isuspgrim  48372  clnbgrgrimlem  48409  clnbgrgrim  48410  isgrtri  48419  isubgr3stgrlem4  48445  grlimgrtri  48479  grlictr  48491  gpgedgvtx0  48537  gpgedg2iv  48543  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  pgn4cyclex  48602  isupwlkg  48613  rngcinvALTV  48752  ringcinvALTV  48786  srhmsubcALTV  48801  mapprop  48822  zlmodzxzadd  48834  domnmsuppn0  48845  ply1mulgsumlem2  48863  lincsum  48905  lincsumcl  48907  lincscmcl  48908  isldepslvec2  48961  digexp  49083  rrx2pnecoorneor  49191  rrx2pnedifcoorneorr  49193  rrx2xpref1o  49194  ehl2eudis0lt  49202  rrx2linest  49218  line2x  49230  itsclc0yqsollem2  49239  seppsepf  49404  thincn0eu  49906