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  3493  cgsex4g  3494  cgsex4gOLD  3495  spc2egv  3565  spc2ed  3567  uneqin  4252  2reu4lem  4485  2reu4  4486  disjpr2  4677  ssunieq  4907  iuneq1  4972  iuneq2  4975  copsex2t  5452  propeqop  5467  opthhausdorff  5477  opthhausdorff0  5478  iunopeqop  5481  soeq2  5568  opbrop  5736  xpsspw  5772  coeq1  5821  coeq2  5822  cnveq  5837  dmeq  5867  sotri  6100  tz7.7  6358  funun  6562  fununfun  6564  fundif  6565  funprg  6570  funtp  6573  2elresin  6639  funssxp  6716  fssres  6726  f1cof1  6766  foun  6818  f1un  6820  resdif  6821  f1oco  6823  fvun  6951  elfvmptrab1w  6995  elfvmptrab1  6996  fvn0ssdmfun  7046  dff3  7072  exfo  7077  fprg  7127  ftpg  7128  f1ounsn  7247  weisoeq2  7331  oprabv  7449  ndmovdistr  7578  ndmovord  7579  brrpssg  7701  eldifpw  7744  iunpw  7747  epweon  7751  bropfvvvv  8071  f1o2ndf1  8101  poseq  8137  fvn0elsupp  8159  smores  8321  tz7.49  8413  tz7.49c  8414  oaord  8511  oeeulem  8565  nnaord  8583  brecop  8783  brecop2  8784  eroveu  8785  ecopovtrn  8793  ixpeq2  8884  undifixp  8907  sbthlem8  9058  sbthlem9  9059  unxpdom  9200  isinf  9207  isinfOLD  9208  f1opwfi  9307  fiin  9373  en2lp  9559  inf3lem3  9583  brttrcl  9666  tcmin  9694  djuexb  9862  alephfp  10061  kmlem16  10119  endjudisj  10122  cofsmo  10222  fin23lem28  10293  axdc3lem2  10404  ac6c4  10434  brdom3  10481  brdom5  10482  brdom4  10483  canthp1lem2  10606  finngch  10608  ordpipq  10895  adderpq  10909  mulerpq  10910  lterpq  10923  genpn0  10956  genpnnp  10958  addclprlem2  10970  addcmpblnr  11022  addsrpr  11028  mulsrpr  11029  addclsr  11036  addasssr  11041  distrsr  11044  0idsr  11050  1idsr  11051  00sr  11052  mulgt0sr  11058  axaddf  11098  axaddass  11109  axdistr  11111  cnegex  11355  recextlem2  11809  difgtsumgt  12495  zaddcl  12573  qaddcl  12924  qmulcl  12926  qreccl  12928  xmulgt0  13243  xrsupsslem  13267  xrinfmsslem  13268  supxrpnf  13278  iccss  13375  difreicc  13445  fzadd2  13520  fzsubel  13521  ssfzunsnext  13530  difelfznle  13603  2ffzeq  13610  nelfzo  13625  fzonmapblen  13669  ubmelfzo  13691  ubmelm1fzo  13724  elfznelfzo  13733  subfzo0  13750  adddivflid  13780  modaddid  13872  modifeq2int  13898  modaddmodup  13899  addmodlteq  13911  fsuppmapnn0fiub  13956  mulexp  14066  mulexpz  14067  leexp1a  14140  faclbnd  14255  hashunx  14351  hashgt23el  14389  wrdeq  14501  ccatcl  14539  swrdnd  14619  swrdnd0  14622  swrdsbslen  14629  swrdspsleq  14630  pfxccat1  14667  swrdswrdlem  14669  pfxccatin12lem2a  14692  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccatin12  14698  swrdccat  14700  reuccatpfxs1  14712  repswswrd  14749  repswccat  14751  cshwidxn  14774  cshweqdif2  14784  2cshwcshw  14791  cshwcshid  14793  cshwcsh2id  14794  f1oun2prg  14883  s2eq2s1eq  14902  s3eqs2s1eq  14904  s3sndisj  14933  s3iunsndisj  14934  sqabsadd  15248  sqabssub  15249  abs2dif  15299  rexanuz  15312  o1of2  15579  o1rlimmul  15585  fsum2dlem  15736  isumltss  15814  fprodser  15915  fprodeq0  15941  fprod2dlem  15946  dvdscmulr  16254  dvdsmulcr  16255  summodnegmod  16256  difmod0  16257  dvds2ln  16259  dvdsflip  16287  divalglem9  16371  gcdcllem3  16471  gcdaddmlem  16494  sqgcd  16532  lcmcllem  16566  lcmabs  16575  lcmgcdlem  16576  lcmgcd  16577  lcmgcdeq  16582  lcmftp  16606  lcmfunsnlem2lem1  16608  qredeq  16627  cncongr1  16637  cncongr2  16638  isprm7  16678  hashgcdlem  16758  dvdsprmpweqle  16857  difsqpwdvds  16858  prmgaplem4  17025  cshwsidrepsw  17064  setsfun0  17142  setsstruct2  17144  xpsfrnel2  17527  isfunc  17826  tsrss  18548  rabsubmgmd  18631  resmgmhm2  18639  mndpfsupp  18694  ismhm0  18717  mhmismgmhm  18718  mndissubm  18734  resmndismnd  18735  resmhm2  18748  submefmnd  18822  sursubmefmnd  18823  injsubmefmnd  18824  grpissubg  19078  gimco  19200  symg2bas  19323  pgrpsubgsymg  19339  symgextf  19347  fvcosymgeq  19359  gsmsymgreqlem1  19360  symgfixf1  19367  efgrelexlema  19679  gsum2dlem1  19900  gsum2dlem2  19901  dvdsr  20271  isrnghmmul  20351  c0ghm  20370  rhmisrnghm  20389  subrngpropd  20477  subrgpropd  20517  rnghmsubcsetclem2  20541  rngcinv  20546  rhmsubcsetclem2  20570  rhmsubcrngclem2  20576  ringcinv  20580  srhmsubc  20589  islmhm2  20945  psgnghm  21489  psgndiflemB  21509  frlmbas3  21685  frlmphl  21690  islindf4  21747  ressmpladd  21936  ressmplmul  21937  mplind  21977  mpomatmul  22333  mavmul0g  22440  1marepvsma1  22470  mdetdiag  22486  slesolvec  22566  cramerimplem2  22571  cramerimplem3  22572  cramerimp  22573  mat2pmatlin  22622  m2pmfzgsumcl  22635  monmatcollpw  22666  pmatcollpw3lem  22670  pmatcollpwscmatlem1  22676  chpmat1dlem  22722  chfacfisf  22741  chfacfisfcpmat  22742  chfacfpmmulgsum2  22752  tgcl  22856  uncld  22928  innei  23012  cnco  23153  uncmp  23290  txbas  23454  txbasval  23493  tx1stc  23537  fbun  23727  infil  23750  fbunfip  23756  filuni  23772  imaelfm  23838  txflf  23893  tsmsfbas  24015  tsmsxp  24042  blin2  24317  nmhmplusg  24645  qtopbaslem  24646  iccntr  24710  ncvspi  25056  ncvs1  25057  unmbl  25438  volfiniun  25448  mbfi1flimlem  25623  ply1idom  26030  logreclem  26672  relogbcxpb  26697  fsumvma2  27125  chpchtsum  27130  dchrelbas3  27149  dchrmulcl  27160  lgsmulsqcoprm  27254  gausslemma2dlem1a  27276  lgsquad2lem2  27296  dchrisum0fmul  27417  dchrisum0lem1  27427  sltres  27574  nocvxminlem  27689  oldlim  27798  madebdayim  27799  madebdaylemlrcut  27810  readdscl  28350  remulscl  28353  ishpg  28686  brcgr  28827  brbtwn2  28832  axcontlem2  28892  uspgredg2v  29151  usgredg2v  29154  usgr2v1e2w  29179  nb3gr2nb  29311  cusgredg  29351  cplgr3v  29362  cusgrop  29365  rusgr1vtx  29516  iswlkg  29541  wlkeq  29562  wlk1walk  29567  uspgr2wlkeq2  29575  uspgr2wlkeqi  29576  cyclnumvtx  29730  crctcshwlkn0lem3  29742  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  wspthneq1eq2  29790  wwlksnextinj  29829  2wlkdlem7  29862  2wlkdlem8  29863  2pthon3v  29873  s3wwlks2on  29886  elwwlks2  29896  elwspths2spth  29897  rusgrnumwwlks  29904  clwlkclwwlklem2a  29927  clwlkclwwlklem3  29930  clwlkclwwlkf1lem2  29934  clwlkclwwlkf1  29939  clwwlknonex2  30038  3wlkdlem3  30090  uhgr3cyclex  30111  cusconngr  30120  eupth0  30143  frgr3v  30204  1to3vfriswmgr  30209  4cycl2v2nb  30218  frgrnbnb  30222  frgrncvvdeq  30238  frgrwopreglem4a  30239  frgrwopreglem5a  30240  frgrwopreglem4  30244  frgrwopreglem5  30250  frgrhash2wsp  30261  numclwwlk1lem2foa  30283  numclwwlk2  30310  blocni  30734  hvsub4  30966  shscli  31246  shscom  31248  spanunsni  31508  spanpr  31509  5oalem2  31584  5oalem3  31585  5oalem5  31587  3oalem1  31591  hoscl  31674  hoadddi  31732  hoadddir  31733  hosub4  31742  lnophsi  31930  hmops  31949  hmopm  31950  adjadd  32022  leop2  32053  leopadd  32061  leopmuli  32062  pjclem4  32128  pj3si  32136  mdslmd1lem2  32255  mdslmd3i  32261  atomli  32311  atcvatlem  32314  chirredlem3  32321  chirredi  32323  atcvat3i  32325  mdsymlem1  32332  mdsymlem5  32336  cdjreui  32361  cdj3i  32370  addltmulALT  32375  hashxpe  32732  domnmuln0rd  33225  mndpluscn  33916  sxbrsigalem5  34279  probfinmeasbALTV  34420  bnj545  34885  bnj546  34886  bnj557  34891  bnj570  34895  bnj594  34902  bnj1001  34949  bnj1118  34974  txpconn  35219  cvmlift2lem10  35299  gonar  35382  lediv2aALT  35664  altopeq12  35950  altxpsspw  35965  funtransport  36019  neibastop1  36347  filnetlem3  36368  lukshef-ax2  36403  arg-ax  36404  nndivsub  36445  bj-nnftht  36729  bj-nnfan  36736  bj-nnfor  36738  copsex2b  37128  isbasisrelowllem1  37343  isbasisrelowllem2  37344  icoreclin  37345  relowlssretop  37351  rdgeqoa  37358  fvineqsnf1  37398  wl-ax11-lem2  37574  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem4  37618  poimirlem26  37640  poimirlem29  37643  poimirlem30  37644  heicant  37649  mblfinlem1  37651  ismblfin  37655  itg2addnclem  37665  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  prdstotbnd  37788  heibor1lem  37803  isdrngo2  37952  divrngidl  38022  pridlc3  38067  linepsubN  39746  pmapsub  39762  elpaddri  39796  paddasslem14  39827  pmapjoin  39846  dvhfvadd  41085  dvhvaddcomN  41090  bcle2d  42167  imacrhmcl  42502  rimco  42506  rmxynorm  42907  monotoddzzfi  42931  acongtr  42967  mpaaeu  43139  oaltublim  43279  omord2lim  43289  cantnftermord  43309  dflim5  43318  omabs2  43321  tfsconcat0i  43334  ofoafo  43345  naddcnff  43351  oaun3lem1  43363  oaun3lem2  43364  pr2cv  43537  brfvrcld2  43681  rfovcnvf1od  43993  ismnushort  44290  nzin  44307  pm10.14  44348  disjrnmpt2  45182  liminfvalxr  45781  etransclem38  46270  cfsetsnfsetf1  47060  tz6.12-afv2  47241  2elfz2melfz  47319  fz0addge0  47320  2ffzoeq  47328  difltmodne  47343  modn0mul  47358  mod2addne  47365  icceuelpartlem  47436  icceuelpart  47437  ich2exprop  47472  sqrtpwpw2p  47539  fmtnoprmfac1lem  47565  fmtnoprmfac1  47566  lighneallem2  47607  divgcdoddALTV  47683  gbowpos  47760  gbowgt5  47763  gboge9  47765  nnsum3primesgbe  47793  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  isuspgrim  47896  clnbgrgrimlem  47933  clnbgrgrim  47934  isgrtri  47942  isubgr3stgrlem4  47968  grlimgrtri  47995  grlictr  48007  gpgedgvtx0  48052  gpgedg2iv  48058  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  pgn4cyclex  48116  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