Theorem anim12i 612

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 595	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  613  anim1i  614  anim2i  616  anifp  1072  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  spc2egv  3612  spc2ed  3614  sseq2  4035  uneqin  4308  2reu4lem  4545  2reu4  4546  disjpr2  4738  ssunieq  4967  iuneq1  5031  iuneq2  5034  copsex2t  5512  propeqop  5526  opthhausdorff  5536  opthhausdorff0  5537  iunopeqop  5540  soeq2  5630  opbrop  5797  xpsspw  5833  coeq1  5882  coeq2  5883  cnveq  5898  dmeq  5928  sotri  6159  tz7.7  6421  funun  6624  fununfun  6626  fundif  6627  funprg  6632  funtp  6635  2elresin  6701  funssxp  6776  fssres  6787  f1cof1  6827  f1coOLD  6829  foun  6880  f1un  6882  resdif  6883  f1oco  6885  fvun  7012  elfvmptrab1w  7056  elfvmptrab1  7057  fvn0ssdmfun  7108  dff3  7134  exfo  7139  fprg  7189  ftpg  7190  weisoeq2  7392  oprabv  7510  ndmovdistr  7639  ndmovord  7640  brrpssg  7760  eldifpw  7803  iunpw  7806  epweon  7810  bropfvvvv  8133  f1o2ndf1  8163  poseq  8199  fvn0elsupp  8221  wfrlem5OLD  8369  smores  8408  tz7.49  8501  tz7.49c  8502  oaord  8603  oeeulem  8657  nnaord  8675  brecop  8868  brecop2  8869  eroveu  8870  ecopovtrn  8878  ixpeq2  8969  undifixp  8992  undomOLD  9126  sbthlem8  9156  sbthlem9  9157  unxpdom  9316  isinf  9323  isinfOLD  9324  f1opwfi  9426  fiin  9491  en2lp  9675  inf3lem3  9699  brttrcl  9782  tcmin  9810  djuexb  9978  alephfp  10177  kmlem16  10235  endjudisj  10238  cofsmo  10338  fin23lem28  10409  axdc3lem2  10520  ac6c4  10550  brdom3  10597  brdom5  10598  brdom4  10599  canthp1lem2  10722  finngch  10724  ordpipq  11011  adderpq  11025  mulerpq  11026  lterpq  11039  genpn0  11072  genpnnp  11074  addclprlem2  11086  addcmpblnr  11138  addsrpr  11144  mulsrpr  11145  addclsr  11152  addasssr  11157  distrsr  11160  0idsr  11166  1idsr  11167  00sr  11168  mulgt0sr  11174  axaddf  11214  axaddass  11225  axdistr  11227  cnegex  11471  recextlem2  11921  difgtsumgt  12606  zaddcl  12683  qaddcl  13030  qmulcl  13032  qreccl  13034  xmulgt0  13345  xrsupsslem  13369  xrinfmsslem  13370  supxrpnf  13380  iccss  13475  difreicc  13544  fzadd2  13619  fzsubel  13620  ssfzunsnext  13629  difelfznle  13699  2ffzeq  13706  nelfzo  13721  fzonmapblen  13762  ubmelfzo  13781  ubmelm1fzo  13813  elfznelfzo  13822  subfzo0  13839  adddivflid  13869  modifeq2int  13984  modaddmodup  13985  addmodlteq  13997  fsuppmapnn0fiub  14042  mulexp  14152  mulexpz  14153  leexp1a  14225  faclbnd  14339  hashunx  14435  hashgt23el  14473  wrdeq  14584  ccatcl  14622  swrdnd  14702  swrdnd0  14705  swrdsbslen  14712  swrdspsleq  14713  pfxccat1  14750  swrdswrdlem  14752  pfxccatin12lem2a  14775  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12  14781  swrdccat  14783  reuccatpfxs1  14795  repswswrd  14832  repswccat  14834  cshwidxn  14857  cshweqdif2  14867  2cshwcshw  14874  cshwcshid  14876  cshwcsh2id  14877  f1oun2prg  14966  s2eq2s1eq  14985  s3eqs2s1eq  14987  s3sndisj  15016  s3iunsndisj  15017  sqabsadd  15331  sqabssub  15332  abs2dif  15381  rexanuz  15394  o1of2  15659  o1rlimmul  15665  fsum2dlem  15818  isumltss  15896  fprodser  15997  fprodeq0  16023  fprod2dlem  16028  dvdscmulr  16333  dvdsmulcr  16334  summodnegmod  16335  dvds2ln  16337  dvdsflip  16365  divalglem9  16449  gcdcllem3  16547  gcdaddmlem  16570  gcdabsOLD  16578  sqgcd  16609  lcmcllem  16643  lcmabs  16652  lcmgcdlem  16653  lcmgcd  16654  lcmgcdeq  16659  lcmftp  16683  lcmfunsnlem2lem1  16685  qredeq  16704  cncongr1  16714  cncongr2  16715  isprm7  16755  hashgcdlem  16835  dvdsprmpweqle  16933  difsqpwdvds  16934  prmgaplem4  17101  cshwsidrepsw  17141  setsfun0  17219  setsstruct2  17221  xpsfrnel2  17624  isfunc  17928  tsrss  18659  rabsubmgmd  18742  resmgmhm2  18750  ismhm0  18825  mhmismgmhm  18826  mndissubm  18842  resmndismnd  18843  resmhm2  18856  submefmnd  18930  sursubmefmnd  18931  injsubmefmnd  18932  grpissubg  19186  gimco  19308  symg2bas  19434  pgrpsubgsymg  19451  symgextf  19459  fvcosymgeq  19471  gsmsymgreqlem1  19472  symgfixf1  19479  efgrelexlema  19791  gsum2dlem1  20012  gsum2dlem2  20013  dvdsr  20388  isrnghmmul  20468  c0ghm  20487  rhmisrnghm  20506  subrngpropd  20594  subrgpropd  20636  rnghmsubcsetclem2  20654  rngcinv  20659  rhmsubcsetclem2  20683  rhmsubcrngclem2  20689  ringcinv  20693  srhmsubc  20702  islmhm2  21060  psgnghm  21621  psgndiflemB  21641  frlmbas3  21819  frlmphl  21824  islindf4  21881  ressmpladd  22070  ressmplmul  22071  mplind  22117  mpomatmul  22473  mavmul0g  22580  1marepvsma1  22610  mdetdiag  22626  slesolvec  22706  cramerimplem2  22711  cramerimplem3  22712  cramerimp  22713  mat2pmatlin  22762  m2pmfzgsumcl  22775  monmatcollpw  22806  pmatcollpw3lem  22810  pmatcollpwscmatlem1  22816  chpmat1dlem  22862  chfacfisf  22881  chfacfisfcpmat  22882  chfacfpmmulgsum2  22892  tgcl  22997  uncld  23070  innei  23154  cnco  23295  uncmp  23432  txbas  23596  txbasval  23635  tx1stc  23679  fbun  23869  infil  23892  fbunfip  23898  filuni  23914  imaelfm  23980  txflf  24035  tsmsfbas  24157  tsmsxp  24184  blin2  24460  nmhmplusg  24799  qtopbaslem  24800  iccntr  24862  ncvspi  25209  ncvs1  25210  unmbl  25591  volfiniun  25601  mbfi1flimlem  25777  ply1idom  26184  logreclem  26823  relogbcxpb  26848  fsumvma2  27276  chpchtsum  27281  dchrelbas3  27300  dchrmulcl  27311  lgsmulsqcoprm  27405  gausslemma2dlem1a  27427  lgsquad2lem2  27447  dchrisum0fmul  27568  dchrisum0lem1  27578  sltres  27725  nocvxminlem  27840  oldlim  27943  madebdayim  27944  madebdaylemlrcut  27955  readdscl  28449  remulscl  28452  ishpg  28785  brcgr  28933  brbtwn2  28938  axcontlem2  28998  uspgredg2v  29259  usgredg2v  29262  usgr2v1e2w  29287  nb3gr2nb  29419  cusgredg  29459  cplgr3v  29470  cusgrop  29473  rusgr1vtx  29624  iswlkg  29649  wlkeq  29670  wlk1walk  29675  uspgr2wlkeq2  29683  uspgr2wlkeqi  29684  crctcshwlkn0lem3  29845  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  wspthneq1eq2  29893  wwlksnextinj  29932  2wlkdlem7  29965  2wlkdlem8  29966  2pthon3v  29976  s3wwlks2on  29989  elwwlks2  29999  elwspths2spth  30000  rusgrnumwwlks  30007  clwlkclwwlklem2a  30030  clwlkclwwlklem3  30033  clwlkclwwlkf1lem2  30037  clwlkclwwlkf1  30042  clwwlknonex2  30141  3wlkdlem3  30193  uhgr3cyclex  30214  cusconngr  30223  eupth0  30246  frgr3v  30307  1to3vfriswmgr  30312  4cycl2v2nb  30321  frgrnbnb  30325  frgrncvvdeq  30341  frgrwopreglem4a  30342  frgrwopreglem5a  30343  frgrwopreglem4  30347  frgrwopreglem5  30353  frgrhash2wsp  30364  numclwwlk1lem2foa  30386  numclwwlk2  30413  blocni  30837  hvsub4  31069  shscli  31349  shscom  31351  spanunsni  31611  spanpr  31612  5oalem2  31687  5oalem3  31688  5oalem5  31690  3oalem1  31694  hoscl  31777  hoadddi  31835  hoadddir  31836  hosub4  31845  lnophsi  32033  hmops  32052  hmopm  32053  adjadd  32125  leop2  32156  leopadd  32164  leopmuli  32165  pjclem4  32231  pj3si  32239  mdslmd1lem2  32358  mdslmd3i  32364  atomli  32414  atcvatlem  32417  chirredlem3  32424  chirredi  32426  atcvat3i  32428  mdsymlem1  32435  mdsymlem5  32439  cdjreui  32464  cdj3i  32473  addltmulALT  32478  hashxpe  32814  domnmuln0rd  33246  mndpluscn  33872  sxbrsigalem5  34253  probfinmeasbALTV  34394  bnj545  34871  bnj546  34872  bnj557  34877  bnj570  34881  bnj594  34888  bnj1001  34935  bnj1118  34960  txpconn  35200  cvmlift2lem10  35280  gonar  35363  lediv2aALT  35645  altopeq12  35926  altxpsspw  35941  funtransport  35995  neibastop1  36325  filnetlem3  36346  lukshef-ax2  36381  arg-ax  36382  nndivsub  36423  bj-nnftht  36707  bj-nnfan  36714  bj-nnfor  36716  copsex2b  37106  isbasisrelowllem1  37321  isbasisrelowllem2  37322  icoreclin  37323  relowlssretop  37329  rdgeqoa  37336  fvineqsnf1  37376  wl-ax11-lem2  37540  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem4  37584  poimirlem26  37606  poimirlem29  37609  poimirlem30  37610  heicant  37615  mblfinlem1  37617  ismblfin  37621  itg2addnclem  37631  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  prdstotbnd  37754  heibor1lem  37769  isdrngo2  37918  divrngidl  37988  pridlc3  38033  linepsubN  39709  pmapsub  39725  elpaddri  39759  paddasslem14  39790  pmapjoin  39809  dvhfvadd  41048  dvhvaddcomN  41053  bcle2d  42136  imacrhmcl  42469  rimco  42473  rmxynorm  42875  monotoddzzfi  42899  acongtr  42935  mpaaeu  43107  oaltublim  43252  omord2lim  43262  cantnftermord  43282  dflim5  43291  omabs2  43294  tfsconcat0i  43307  ofoafo  43318  naddcnff  43324  oaun3lem1  43336  oaun3lem2  43337  pr2cv  43510  brfvrcld2  43654  rfovcnvf1od  43966  ismnushort  44270  nzin  44287  pm10.14  44328  disjrnmpt2  45095  liminfvalxr  45704  etransclem38  46193  cfsetsnfsetf1  46974  tz6.12-afv2  47155  2elfz2melfz  47233  fz0addge0  47234  2ffzoeq  47242  icceuelpartlem  47309  icceuelpart  47310  ich2exprop  47345  sqrtpwpw2p  47412  fmtnoprmfac1lem  47438  fmtnoprmfac1  47439  lighneallem2  47480  divgcdoddALTV  47556  gbowpos  47633  gbowgt5  47636  gboge9  47638  nnsum3primesgbe  47666  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  clnbgrgrimlem  47785  clnbgrgrim  47786  isgrtri  47794  grlimgrtri  47820  grlictr  47832  isupwlkg  47860  rngcinvALTV  47999  ringcinvALTV  48033  srhmsubcALTV  48048  mapprop  48071  zlmodzxzadd  48083  domnmsuppn0  48094  mndpfsupp  48101  ply1mulgsumlem2  48116  lincsum  48158  lincsumcl  48160  lincscmcl  48161  isldepslvec2  48214  modn0mul  48254  digexp  48341  rrx2pnecoorneor  48449  rrx2pnedifcoorneorr  48451  rrx2xpref1o  48452  ehl2eudis0lt  48460  rrx2linest  48476  line2x  48488  itsclc0yqsollem2  48497  seppsepf  48608  thincn0eu  48699