Theorem anim12i 611

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  anim12ci  612  anim1i  613  anim2i  615  anifp  1068  cgsex2g  3518  cgsex4g  3519  cgsex4gOLD  3520  cgsex4gOLDOLD  3521  spc2egv  3588  spc2ed  3590  sseq2  4007  uneqin  4277  2reu4lem  4524  2reu4  4525  disjpr2  4716  ssunieq  4946  iuneq1  5012  iuneq2  5015  copsex2t  5491  propeqop  5506  opthhausdorff  5516  opthhausdorff0  5517  iunopeqop  5520  soeq2  5609  opbrop  5772  xpsspw  5808  coeq1  5856  coeq2  5857  cnveq  5872  dmeq  5902  sotri  6127  tz7.7  6389  funun  6593  fununfun  6595  fundif  6596  funprg  6601  funtp  6604  2elresin  6670  funssxp  6745  fssres  6756  f1cof1  6797  f1coOLD  6799  foun  6850  f1un  6852  resdif  6853  f1oco  6855  fvun  6980  elfvmptrab1w  7023  elfvmptrab1  7024  fvn0ssdmfun  7075  dff3  7100  exfo  7105  fprg  7154  ftpg  7155  weisoeq2  7355  oprabv  7471  ndmovdistr  7598  ndmovord  7599  brrpssg  7717  eldifpw  7757  iunpw  7760  epweon  7764  bropfvvvv  8080  f1o2ndf1  8110  poseq  8146  fvn0elsupp  8167  wfrlem5OLD  8315  smores  8354  tz7.49  8447  tz7.49c  8448  oaord  8549  oeeulem  8603  nnaord  8621  brecop  8806  brecop2  8807  eroveu  8808  ecopovtrn  8816  ixpeq2  8907  undifixp  8930  undomOLD  9062  sbthlem8  9092  sbthlem9  9093  unxpdom  9255  isinf  9262  isinfOLD  9263  f1opwfi  9358  fiin  9419  en2lp  9603  inf3lem3  9627  brttrcl  9710  tcmin  9738  djuexb  9906  alephfp  10105  kmlem16  10162  endjudisj  10165  cofsmo  10266  fin23lem28  10337  axdc3lem2  10448  ac6c4  10478  brdom3  10525  brdom5  10526  brdom4  10527  canthp1lem2  10650  finngch  10652  ordpipq  10939  adderpq  10953  mulerpq  10954  lterpq  10967  genpn0  11000  genpnnp  11002  addclprlem2  11014  addcmpblnr  11066  addsrpr  11072  mulsrpr  11073  addclsr  11080  addasssr  11085  distrsr  11088  0idsr  11094  1idsr  11095  00sr  11096  mulgt0sr  11102  axaddf  11142  axaddass  11153  axdistr  11155  cnegex  11399  recextlem2  11849  difgtsumgt  12529  zaddcl  12606  qaddcl  12953  qmulcl  12955  qreccl  12957  xmulgt0  13266  xrsupsslem  13290  xrinfmsslem  13291  supxrpnf  13301  iccss  13396  difreicc  13465  fzadd2  13540  fzsubel  13541  ssfzunsnext  13550  difelfznle  13619  2ffzeq  13626  nelfzo  13641  fzonmapblen  13682  ubmelfzo  13701  ubmelm1fzo  13732  elfznelfzo  13741  subfzo0  13758  adddivflid  13787  modifeq2int  13902  modaddmodup  13903  addmodlteq  13915  fsuppmapnn0fiub  13960  mulexp  14071  mulexpz  14072  leexp1a  14144  faclbnd  14254  hashunx  14350  hashgt23el  14388  wrdeq  14490  ccatcl  14528  swrdnd  14608  swrdnd0  14611  swrdsbslen  14618  swrdspsleq  14619  pfxccat1  14656  swrdswrdlem  14658  pfxccatin12lem2a  14681  swrdccatin2  14683  pfxccatin12lem2  14685  pfxccatin12  14687  swrdccat  14689  reuccatpfxs1  14701  repswswrd  14738  repswccat  14740  cshwidxn  14763  cshweqdif2  14773  2cshwcshw  14780  cshwcshid  14782  cshwcsh2id  14783  f1oun2prg  14872  s2eq2s1eq  14891  s3eqs2s1eq  14893  s3sndisj  14918  s3iunsndisj  14919  sqabsadd  15233  sqabssub  15234  abs2dif  15283  rexanuz  15296  o1of2  15561  o1rlimmul  15567  fsum2dlem  15720  isumltss  15798  fprodser  15897  fprodeq0  15923  fprod2dlem  15928  dvdscmulr  16232  dvdsmulcr  16233  summodnegmod  16234  dvds2ln  16236  dvdsflip  16264  divalglem9  16348  gcdcllem3  16446  gcdaddmlem  16469  gcdabsOLD  16477  sqgcd  16506  lcmcllem  16537  lcmabs  16546  lcmgcdlem  16547  lcmgcd  16548  lcmgcdeq  16553  lcmftp  16577  lcmfunsnlem2lem1  16579  qredeq  16598  cncongr1  16608  cncongr2  16609  isprm7  16649  hashgcdlem  16725  dvdsprmpweqle  16823  difsqpwdvds  16824  prmgaplem4  16991  cshwsidrepsw  17031  setsfun0  17109  setsstruct2  17111  xpsfrnel2  17514  isfunc  17818  tsrss  18546  rabsubmgmd  18629  resmgmhm2  18637  ismhm0  18712  mhmismgmhm  18713  mndissubm  18724  resmndismnd  18725  resmhm2  18738  submefmnd  18812  sursubmefmnd  18813  injsubmefmnd  18814  grpissubg  19062  gimco  19182  symg2bas  19301  pgrpsubgsymg  19318  symgextf  19326  fvcosymgeq  19338  gsmsymgreqlem1  19339  symgfixf1  19346  efgrelexlema  19658  gsum2dlem1  19879  gsum2dlem2  19880  dvdsr  20253  isrnghmmul  20333  c0ghm  20352  rhmisrnghm  20371  subrngpropd  20456  subrgpropd  20498  islmhm2  20793  psgnghm  21352  psgndiflemB  21372  frlmbas3  21550  frlmphl  21555  islindf4  21612  ressmpladd  21803  ressmplmul  21804  mplind  21850  mpomatmul  22168  mavmul0g  22275  1marepvsma1  22305  mdetdiag  22321  slesolvec  22401  cramerimplem2  22406  cramerimplem3  22407  cramerimp  22408  mat2pmatlin  22457  m2pmfzgsumcl  22470  monmatcollpw  22501  pmatcollpw3lem  22505  pmatcollpwscmatlem1  22511  chpmat1dlem  22557  chfacfisf  22576  chfacfisfcpmat  22577  chfacfpmmulgsum2  22587  tgcl  22692  uncld  22765  innei  22849  cnco  22990  uncmp  23127  txbas  23291  txbasval  23330  tx1stc  23374  fbun  23564  infil  23587  fbunfip  23593  filuni  23609  imaelfm  23675  txflf  23730  tsmsfbas  23852  tsmsxp  23879  blin2  24155  nmhmplusg  24494  qtopbaslem  24495  iccntr  24557  ncvspi  24904  ncvs1  24905  unmbl  25286  volfiniun  25296  mbfi1flimlem  25472  ply1idom  25877  logreclem  26503  relogbcxpb  26528  fsumvma2  26953  chpchtsum  26958  dchrelbas3  26977  dchrmulcl  26988  lgsmulsqcoprm  27082  gausslemma2dlem1a  27104  lgsquad2lem2  27124  dchrisum0fmul  27245  dchrisum0lem1  27255  sltres  27401  nocvxminlem  27515  oldlim  27618  madebdayim  27619  madebdaylemlrcut  27630  ishpg  28277  brcgr  28425  brbtwn2  28430  axcontlem2  28490  uspgredg2v  28748  usgredg2v  28751  usgr2v1e2w  28776  nb3gr2nb  28908  cusgredg  28948  cplgr3v  28959  cusgrop  28962  rusgr1vtx  29112  iswlkg  29137  wlkeq  29158  wlk1walk  29163  uspgr2wlkeq2  29171  uspgr2wlkeqi  29172  crctcshwlkn0lem3  29333  crctcshwlkn0lem4  29334  crctcshwlkn0lem5  29335  wspthneq1eq2  29381  wwlksnextinj  29420  2wlkdlem7  29453  2wlkdlem8  29454  2pthon3v  29464  s3wwlks2on  29477  elwwlks2  29487  elwspths2spth  29488  rusgrnumwwlks  29495  clwlkclwwlklem2a  29518  clwlkclwwlklem3  29521  clwlkclwwlkf1lem2  29525  clwlkclwwlkf1  29530  clwwlknonex2  29629  3wlkdlem3  29681  uhgr3cyclex  29702  cusconngr  29711  eupth0  29734  frgr3v  29795  1to3vfriswmgr  29800  4cycl2v2nb  29809  frgrnbnb  29813  frgrncvvdeq  29829  frgrwopreglem4a  29830  frgrwopreglem5a  29831  frgrwopreglem4  29835  frgrwopreglem5  29841  frgrhash2wsp  29852  numclwwlk1lem2foa  29874  numclwwlk2  29901  blocni  30325  hvsub4  30557  shscli  30837  shscom  30839  spanunsni  31099  spanpr  31100  5oalem2  31175  5oalem3  31176  5oalem5  31178  3oalem1  31182  hoscl  31265  hoadddi  31323  hoadddir  31324  hosub4  31333  lnophsi  31521  hmops  31540  hmopm  31541  adjadd  31613  leop2  31644  leopadd  31652  leopmuli  31653  pjclem4  31719  pj3si  31727  mdslmd1lem2  31846  mdslmd3i  31852  atomli  31902  atcvatlem  31905  chirredlem3  31912  chirredi  31914  atcvat3i  31916  mdsymlem1  31923  mdsymlem5  31927  cdjreui  31952  cdj3i  31961  addltmulALT  31966  hashxpe  32286  mndpluscn  33204  sxbrsigalem5  33585  probfinmeasbALTV  33726  bnj545  34204  bnj546  34205  bnj557  34210  bnj570  34214  bnj594  34221  bnj1001  34268  bnj1118  34293  txpconn  34521  cvmlift2lem10  34601  gonar  34684  lediv2aALT  34960  altopeq12  35238  altxpsspw  35253  funtransport  35307  neibastop1  35547  filnetlem3  35568  lukshef-ax2  35603  arg-ax  35604  nndivsub  35645  bj-nnftht  35922  bj-nnfan  35929  bj-nnfor  35931  copsex2b  36324  isbasisrelowllem1  36539  isbasisrelowllem2  36540  icoreclin  36541  relowlssretop  36547  rdgeqoa  36554  fvineqsnf1  36594  wl-ax11-lem2  36751  matunitlindflem1  36787  matunitlindflem2  36788  poimirlem4  36795  poimirlem26  36817  poimirlem29  36820  poimirlem30  36821  heicant  36826  mblfinlem1  36828  ismblfin  36832  itg2addnclem  36842  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  prdstotbnd  36965  heibor1lem  36980  isdrngo2  37129  divrngidl  37199  pridlc3  37244  linepsubN  38926  pmapsub  38942  elpaddri  38976  paddasslem14  39007  pmapjoin  39026  dvhfvadd  40265  dvhvaddcomN  40270  andiff  41325  imacrhmcl  41393  rimco  41397  rmxynorm  41959  monotoddzzfi  41983  acongtr  42019  mpaaeu  42194  oaltublim  42342  omord2lim  42352  cantnftermord  42372  dflim5  42381  omabs2  42384  tfsconcat0i  42397  ofoafo  42408  naddcnff  42414  oaun3lem1  42426  oaun3lem2  42427  pr2cv  42601  brfvrcld2  42745  rfovcnvf1od  43057  ismnushort  43362  nzin  43379  pm10.14  43420  disjrnmpt2  44185  liminfvalxr  44797  etransclem38  45286  cfsetsnfsetf1  46067  tz6.12-afv2  46246  2elfz2melfz  46324  fz0addge0  46325  2ffzoeq  46334  icceuelpartlem  46401  icceuelpart  46402  ich2exprop  46437  sqrtpwpw2p  46504  fmtnoprmfac1lem  46530  fmtnoprmfac1  46531  lighneallem2  46572  divgcdoddALTV  46648  gbowpos  46725  gbowgt5  46728  gboge9  46730  nnsum3primesgbe  46758  bgoldbtbndlem2  46772  bgoldbtbndlem3  46773  isupwlkg  46813  rnghmsubcsetclem2  46962  rngcinv  46967  rngcinvALTV  46979  rhmsubcsetclem2  47008  rhmsubcrngclem2  47014  ringcinv  47018  ringcinvALTV  47042  srhmsubc  47062  srhmsubcALTV  47080  mapprop  47110  zlmodzxzadd  47122  domnmsuppn0  47133  mndpfsupp  47140  ply1mulgsumlem2  47155  lincsum  47197  lincsumcl  47199  lincscmcl  47200  isldepslvec2  47253  modn0mul  47293  digexp  47380  rrx2pnecoorneor  47488  rrx2pnedifcoorneorr  47490  rrx2xpref1o  47491  ehl2eudis0lt  47499  rrx2linest  47515  line2x  47527  itsclc0yqsollem2  47536  seppsepf  47648  thincn0eu  47739