Theorem anim12i 613

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 596	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  614  anim1i  615  anim2i  617  anifp  1071  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  spc2egv  3556  spc2ed  3558  uneqin  4242  2reu4lem  4475  2reu4  4476  disjpr2  4667  ssunieq  4896  iuneq1  4961  iuneq2  4964  copsex2t  5439  propeqop  5454  opthhausdorff  5464  opthhausdorff0  5465  iunopeqop  5468  soeq2  5553  opbrop  5721  xpsspw  5756  coeq1  5804  coeq2  5805  cnveq  5820  dmeq  5850  sotri  6080  tz7.7  6337  funun  6532  fununfun  6534  fundif  6535  funprg  6540  funtp  6543  2elresin  6607  funssxp  6684  fssres  6694  f1cof1  6734  foun  6786  f1un  6788  resdif  6789  f1oco  6791  fvun  6917  elfvmptrab1w  6961  elfvmptrab1  6962  fvn0ssdmfun  7012  dff3  7038  exfo  7043  fprg  7093  ftpg  7094  f1ounsn  7213  weisoeq2  7297  oprabv  7413  ndmovdistr  7542  ndmovord  7543  brrpssg  7665  eldifpw  7708  iunpw  7711  epweon  7715  bropfvvvv  8032  f1o2ndf1  8062  poseq  8098  fvn0elsupp  8120  smores  8282  tz7.49  8374  tz7.49c  8375  oaord  8472  oeeulem  8526  nnaord  8544  brecop  8744  brecop2  8745  eroveu  8746  ecopovtrn  8754  ixpeq2  8845  undifixp  8868  sbthlem8  9018  sbthlem9  9019  unxpdom  9158  isinf  9165  isinfOLD  9166  f1opwfi  9265  fiin  9331  en2lp  9521  inf3lem3  9545  brttrcl  9628  tcmin  9656  djuexb  9824  alephfp  10021  kmlem16  10079  endjudisj  10082  cofsmo  10182  fin23lem28  10253  axdc3lem2  10364  ac6c4  10394  brdom3  10441  brdom5  10442  brdom4  10443  canthp1lem2  10566  finngch  10568  ordpipq  10855  adderpq  10869  mulerpq  10870  lterpq  10883  genpn0  10916  genpnnp  10918  addclprlem2  10930  addcmpblnr  10982  addsrpr  10988  mulsrpr  10989  addclsr  10996  addasssr  11001  distrsr  11004  0idsr  11010  1idsr  11011  00sr  11012  mulgt0sr  11018  axaddf  11058  axaddass  11069  axdistr  11071  cnegex  11315  recextlem2  11769  difgtsumgt  12455  zaddcl  12533  qaddcl  12884  qmulcl  12886  qreccl  12888  xmulgt0  13203  xrsupsslem  13227  xrinfmsslem  13228  supxrpnf  13238  iccss  13335  difreicc  13405  fzadd2  13480  fzsubel  13481  ssfzunsnext  13490  difelfznle  13563  2ffzeq  13570  nelfzo  13585  fzonmapblen  13629  ubmelfzo  13651  ubmelm1fzo  13684  elfznelfzo  13693  subfzo0  13710  adddivflid  13740  modaddid  13832  modifeq2int  13858  modaddmodup  13859  addmodlteq  13871  fsuppmapnn0fiub  13916  mulexp  14026  mulexpz  14027  leexp1a  14100  faclbnd  14215  hashunx  14311  hashgt23el  14349  wrdeq  14461  ccatcl  14499  swrdnd  14579  swrdnd0  14582  swrdsbslen  14589  swrdspsleq  14590  pfxccat1  14626  swrdswrdlem  14628  pfxccatin12lem2a  14651  swrdccatin2  14653  pfxccatin12lem2  14655  pfxccatin12  14657  swrdccat  14659  reuccatpfxs1  14671  repswswrd  14708  repswccat  14710  cshwidxn  14733  cshweqdif2  14743  2cshwcshw  14750  cshwcshid  14752  cshwcsh2id  14753  f1oun2prg  14842  s2eq2s1eq  14861  s3eqs2s1eq  14863  s3sndisj  14892  s3iunsndisj  14893  sqabsadd  15207  sqabssub  15208  abs2dif  15258  rexanuz  15271  o1of2  15538  o1rlimmul  15544  fsum2dlem  15695  isumltss  15773  fprodser  15874  fprodeq0  15900  fprod2dlem  15905  dvdscmulr  16213  dvdsmulcr  16214  summodnegmod  16215  difmod0  16216  dvds2ln  16218  dvdsflip  16246  divalglem9  16330  gcdcllem3  16430  gcdaddmlem  16453  sqgcd  16491  lcmcllem  16525  lcmabs  16534  lcmgcdlem  16535  lcmgcd  16536  lcmgcdeq  16541  lcmftp  16565  lcmfunsnlem2lem1  16567  qredeq  16586  cncongr1  16596  cncongr2  16597  isprm7  16637  hashgcdlem  16717  dvdsprmpweqle  16816  difsqpwdvds  16817  prmgaplem4  16984  cshwsidrepsw  17023  setsfun0  17101  setsstruct2  17103  xpsfrnel2  17486  isfunc  17789  tsrss  18513  rabsubmgmd  18596  resmgmhm2  18604  mndpfsupp  18659  ismhm0  18682  mhmismgmhm  18683  mndissubm  18699  resmndismnd  18700  resmhm2  18713  submefmnd  18787  sursubmefmnd  18788  injsubmefmnd  18789  grpissubg  19043  gimco  19165  symg2bas  19290  pgrpsubgsymg  19306  symgextf  19314  fvcosymgeq  19326  gsmsymgreqlem1  19327  symgfixf1  19334  efgrelexlema  19646  gsum2dlem1  19867  gsum2dlem2  19868  dvdsr  20265  isrnghmmul  20345  c0ghm  20364  rhmisrnghm  20383  subrngpropd  20471  subrgpropd  20511  rnghmsubcsetclem2  20535  rngcinv  20540  rhmsubcsetclem2  20564  rhmsubcrngclem2  20570  ringcinv  20574  srhmsubc  20583  islmhm2  20960  psgnghm  21505  psgndiflemB  21525  frlmbas3  21701  frlmphl  21706  islindf4  21763  ressmpladd  21952  ressmplmul  21953  mplind  21993  mpomatmul  22349  mavmul0g  22456  1marepvsma1  22486  mdetdiag  22502  slesolvec  22582  cramerimplem2  22587  cramerimplem3  22588  cramerimp  22589  mat2pmatlin  22638  m2pmfzgsumcl  22651  monmatcollpw  22682  pmatcollpw3lem  22686  pmatcollpwscmatlem1  22692  chpmat1dlem  22738  chfacfisf  22757  chfacfisfcpmat  22758  chfacfpmmulgsum2  22768  tgcl  22872  uncld  22944  innei  23028  cnco  23169  uncmp  23306  txbas  23470  txbasval  23509  tx1stc  23553  fbun  23743  infil  23766  fbunfip  23772  filuni  23788  imaelfm  23854  txflf  23909  tsmsfbas  24031  tsmsxp  24058  blin2  24333  nmhmplusg  24661  qtopbaslem  24662  iccntr  24726  ncvspi  25072  ncvs1  25073  unmbl  25454  volfiniun  25464  mbfi1flimlem  25639  ply1idom  26046  logreclem  26688  relogbcxpb  26713  fsumvma2  27141  chpchtsum  27146  dchrelbas3  27165  dchrmulcl  27176  lgsmulsqcoprm  27270  gausslemma2dlem1a  27292  lgsquad2lem2  27312  dchrisum0fmul  27433  dchrisum0lem1  27443  sltres  27590  nocvxminlem  27706  oldlim  27819  madebdayim  27820  madebdaylemlrcut  27831  readdscl  28386  remulscl  28389  ishpg  28722  brcgr  28863  brbtwn2  28868  axcontlem2  28928  uspgredg2v  29187  usgredg2v  29190  usgr2v1e2w  29215  nb3gr2nb  29347  cusgredg  29387  cplgr3v  29398  cusgrop  29401  rusgr1vtx  29552  iswlkg  29577  wlkeq  29597  wlk1walk  29602  uspgr2wlkeq2  29610  uspgr2wlkeqi  29611  cyclnumvtx  29763  crctcshwlkn0lem3  29775  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  wspthneq1eq2  29823  wwlksnextinj  29862  2wlkdlem7  29895  2wlkdlem8  29896  2pthon3v  29906  s3wwlks2on  29919  elwwlks2  29929  elwspths2spth  29930  rusgrnumwwlks  29937  clwlkclwwlklem2a  29960  clwlkclwwlklem3  29963  clwlkclwwlkf1lem2  29967  clwlkclwwlkf1  29972  clwwlknonex2  30071  3wlkdlem3  30123  uhgr3cyclex  30144  cusconngr  30153  eupth0  30176  frgr3v  30237  1to3vfriswmgr  30242  4cycl2v2nb  30251  frgrnbnb  30255  frgrncvvdeq  30271  frgrwopreglem4a  30272  frgrwopreglem5a  30273  frgrwopreglem4  30277  frgrwopreglem5  30283  frgrhash2wsp  30294  numclwwlk1lem2foa  30316  numclwwlk2  30343  blocni  30767  hvsub4  30999  shscli  31279  shscom  31281  spanunsni  31541  spanpr  31542  5oalem2  31617  5oalem3  31618  5oalem5  31620  3oalem1  31624  hoscl  31707  hoadddi  31765  hoadddir  31766  hosub4  31775  lnophsi  31963  hmops  31982  hmopm  31983  adjadd  32055  leop2  32086  leopadd  32094  leopmuli  32095  pjclem4  32161  pj3si  32169  mdslmd1lem2  32288  mdslmd3i  32294  atomli  32344  atcvatlem  32347  chirredlem3  32354  chirredi  32356  atcvat3i  32358  mdsymlem1  32365  mdsymlem5  32369  cdjreui  32394  cdj3i  32403  addltmulALT  32408  hashxpe  32765  domnmuln0rd  33227  mndpluscn  33895  sxbrsigalem5  34258  probfinmeasbALTV  34399  bnj545  34864  bnj546  34865  bnj557  34870  bnj570  34874  bnj594  34881  bnj1001  34928  bnj1118  34953  txpconn  35207  cvmlift2lem10  35287  gonar  35370  lediv2aALT  35652  altopeq12  35938  altxpsspw  35953  funtransport  36007  neibastop1  36335  filnetlem3  36356  lukshef-ax2  36391  arg-ax  36392  nndivsub  36433  bj-nnftht  36717  bj-nnfan  36724  bj-nnfor  36726  copsex2b  37116  isbasisrelowllem1  37331  isbasisrelowllem2  37332  icoreclin  37333  relowlssretop  37339  rdgeqoa  37346  fvineqsnf1  37386  wl-ax11-lem2  37562  matunitlindflem1  37598  matunitlindflem2  37599  poimirlem4  37606  poimirlem26  37628  poimirlem29  37631  poimirlem30  37632  heicant  37637  mblfinlem1  37639  ismblfin  37643  itg2addnclem  37653  ftc1anclem6  37680  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  prdstotbnd  37776  heibor1lem  37791  isdrngo2  37940  divrngidl  38010  pridlc3  38055  linepsubN  39734  pmapsub  39750  elpaddri  39784  paddasslem14  39815  pmapjoin  39834  dvhfvadd  41073  dvhvaddcomN  41078  bcle2d  42155  imacrhmcl  42490  rimco  42494  rmxynorm  42894  monotoddzzfi  42918  acongtr  42954  mpaaeu  43126  oaltublim  43266  omord2lim  43276  cantnftermord  43296  dflim5  43305  omabs2  43308  tfsconcat0i  43321  ofoafo  43332  naddcnff  43338  oaun3lem1  43350  oaun3lem2  43351  pr2cv  43524  brfvrcld2  43668  rfovcnvf1od  43980  ismnushort  44277  nzin  44294  pm10.14  44335  disjrnmpt2  45169  liminfvalxr  45768  etransclem38  46257  cfsetsnfsetf1  47047  tz6.12-afv2  47228  2elfz2melfz  47306  fz0addge0  47307  2ffzoeq  47315  difltmodne  47330  modn0mul  47345  mod2addne  47352  icceuelpartlem  47423  icceuelpart  47424  ich2exprop  47459  sqrtpwpw2p  47526  fmtnoprmfac1lem  47552  fmtnoprmfac1  47553  lighneallem2  47594  divgcdoddALTV  47670  gbowpos  47747  gbowgt5  47750  gboge9  47752  nnsum3primesgbe  47780  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  isuspgrim  47884  clnbgrgrimlem  47921  clnbgrgrim  47922  isgrtri  47931  isubgr3stgrlem4  47957  grlimgrtri  47991  grlictr  48003  gpgedgvtx0  48049  gpgedg2iv  48055  gpg5nbgrvtx03star  48068  gpg5nbgr3star  48069  pgnbgreunbgrlem3  48106  pgnbgreunbgrlem6  48112  pgn4cyclex  48114  isupwlkg  48125  rngcinvALTV  48264  ringcinvALTV  48298  srhmsubcALTV  48313  mapprop  48334  zlmodzxzadd  48346  domnmsuppn0  48357  ply1mulgsumlem2  48376  lincsum  48418  lincsumcl  48420  lincscmcl  48421  isldepslvec2  48474  digexp  48596  rrx2pnecoorneor  48704  rrx2pnedifcoorneorr  48706  rrx2xpref1o  48707  ehl2eudis0lt  48715  rrx2linest  48731  line2x  48743  itsclc0yqsollem2  48752  seppsepf  48917  thincn0eu  49420