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  3496  cgsex4g  3497  cgsex4gOLD  3498  spc2egv  3568  spc2ed  3570  uneqin  4255  2reu4lem  4488  2reu4  4489  disjpr2  4680  ssunieq  4910  iuneq1  4975  iuneq2  4978  copsex2t  5455  propeqop  5470  opthhausdorff  5480  opthhausdorff0  5481  iunopeqop  5484  soeq2  5571  opbrop  5739  xpsspw  5775  coeq1  5824  coeq2  5825  cnveq  5840  dmeq  5870  sotri  6103  tz7.7  6361  funun  6565  fununfun  6567  fundif  6568  funprg  6573  funtp  6576  2elresin  6642  funssxp  6719  fssres  6729  f1cof1  6769  foun  6821  f1un  6823  resdif  6824  f1oco  6826  fvun  6954  elfvmptrab1w  6998  elfvmptrab1  6999  fvn0ssdmfun  7049  dff3  7075  exfo  7080  fprg  7130  ftpg  7131  f1ounsn  7250  weisoeq2  7334  oprabv  7452  ndmovdistr  7581  ndmovord  7582  brrpssg  7704  eldifpw  7747  iunpw  7750  epweon  7754  bropfvvvv  8074  f1o2ndf1  8104  poseq  8140  fvn0elsupp  8162  smores  8324  tz7.49  8416  tz7.49c  8417  oaord  8514  oeeulem  8568  nnaord  8586  brecop  8786  brecop2  8787  eroveu  8788  ecopovtrn  8796  ixpeq2  8887  undifixp  8910  undomOLD  9034  sbthlem8  9064  sbthlem9  9065  unxpdom  9207  isinf  9214  isinfOLD  9215  f1opwfi  9314  fiin  9380  en2lp  9566  inf3lem3  9590  brttrcl  9673  tcmin  9701  djuexb  9869  alephfp  10068  kmlem16  10126  endjudisj  10129  cofsmo  10229  fin23lem28  10300  axdc3lem2  10411  ac6c4  10441  brdom3  10488  brdom5  10489  brdom4  10490  canthp1lem2  10613  finngch  10615  ordpipq  10902  adderpq  10916  mulerpq  10917  lterpq  10930  genpn0  10963  genpnnp  10965  addclprlem2  10977  addcmpblnr  11029  addsrpr  11035  mulsrpr  11036  addclsr  11043  addasssr  11048  distrsr  11051  0idsr  11057  1idsr  11058  00sr  11059  mulgt0sr  11065  axaddf  11105  axaddass  11116  axdistr  11118  cnegex  11362  recextlem2  11816  difgtsumgt  12502  zaddcl  12580  qaddcl  12931  qmulcl  12933  qreccl  12935  xmulgt0  13250  xrsupsslem  13274  xrinfmsslem  13275  supxrpnf  13285  iccss  13382  difreicc  13452  fzadd2  13527  fzsubel  13528  ssfzunsnext  13537  difelfznle  13610  2ffzeq  13617  nelfzo  13632  fzonmapblen  13676  ubmelfzo  13698  ubmelm1fzo  13731  elfznelfzo  13740  subfzo0  13757  adddivflid  13787  modaddid  13879  modifeq2int  13905  modaddmodup  13906  addmodlteq  13918  fsuppmapnn0fiub  13963  mulexp  14073  mulexpz  14074  leexp1a  14147  faclbnd  14262  hashunx  14358  hashgt23el  14396  wrdeq  14508  ccatcl  14546  swrdnd  14626  swrdnd0  14629  swrdsbslen  14636  swrdspsleq  14637  pfxccat1  14674  swrdswrdlem  14676  pfxccatin12lem2a  14699  swrdccatin2  14701  pfxccatin12lem2  14703  pfxccatin12  14705  swrdccat  14707  reuccatpfxs1  14719  repswswrd  14756  repswccat  14758  cshwidxn  14781  cshweqdif2  14791  2cshwcshw  14798  cshwcshid  14800  cshwcsh2id  14801  f1oun2prg  14890  s2eq2s1eq  14909  s3eqs2s1eq  14911  s3sndisj  14940  s3iunsndisj  14941  sqabsadd  15255  sqabssub  15256  abs2dif  15306  rexanuz  15319  o1of2  15586  o1rlimmul  15592  fsum2dlem  15743  isumltss  15821  fprodser  15922  fprodeq0  15948  fprod2dlem  15953  dvdscmulr  16261  dvdsmulcr  16262  summodnegmod  16263  difmod0  16264  dvds2ln  16266  dvdsflip  16294  divalglem9  16378  gcdcllem3  16478  gcdaddmlem  16501  sqgcd  16539  lcmcllem  16573  lcmabs  16582  lcmgcdlem  16583  lcmgcd  16584  lcmgcdeq  16589  lcmftp  16613  lcmfunsnlem2lem1  16615  qredeq  16634  cncongr1  16644  cncongr2  16645  isprm7  16685  hashgcdlem  16765  dvdsprmpweqle  16864  difsqpwdvds  16865  prmgaplem4  17032  cshwsidrepsw  17071  setsfun0  17149  setsstruct2  17151  xpsfrnel2  17534  isfunc  17833  tsrss  18555  rabsubmgmd  18638  resmgmhm2  18646  mndpfsupp  18701  ismhm0  18724  mhmismgmhm  18725  mndissubm  18741  resmndismnd  18742  resmhm2  18755  submefmnd  18829  sursubmefmnd  18830  injsubmefmnd  18831  grpissubg  19085  gimco  19207  symg2bas  19330  pgrpsubgsymg  19346  symgextf  19354  fvcosymgeq  19366  gsmsymgreqlem1  19367  symgfixf1  19374  efgrelexlema  19686  gsum2dlem1  19907  gsum2dlem2  19908  dvdsr  20278  isrnghmmul  20358  c0ghm  20377  rhmisrnghm  20396  subrngpropd  20484  subrgpropd  20524  rnghmsubcsetclem2  20548  rngcinv  20553  rhmsubcsetclem2  20577  rhmsubcrngclem2  20583  ringcinv  20587  srhmsubc  20596  islmhm2  20952  psgnghm  21496  psgndiflemB  21516  frlmbas3  21692  frlmphl  21697  islindf4  21754  ressmpladd  21943  ressmplmul  21944  mplind  21984  mpomatmul  22340  mavmul0g  22447  1marepvsma1  22477  mdetdiag  22493  slesolvec  22573  cramerimplem2  22578  cramerimplem3  22579  cramerimp  22580  mat2pmatlin  22629  m2pmfzgsumcl  22642  monmatcollpw  22673  pmatcollpw3lem  22677  pmatcollpwscmatlem1  22683  chpmat1dlem  22729  chfacfisf  22748  chfacfisfcpmat  22749  chfacfpmmulgsum2  22759  tgcl  22863  uncld  22935  innei  23019  cnco  23160  uncmp  23297  txbas  23461  txbasval  23500  tx1stc  23544  fbun  23734  infil  23757  fbunfip  23763  filuni  23779  imaelfm  23845  txflf  23900  tsmsfbas  24022  tsmsxp  24049  blin2  24324  nmhmplusg  24652  qtopbaslem  24653  iccntr  24717  ncvspi  25063  ncvs1  25064  unmbl  25445  volfiniun  25455  mbfi1flimlem  25630  ply1idom  26037  logreclem  26679  relogbcxpb  26704  fsumvma2  27132  chpchtsum  27137  dchrelbas3  27156  dchrmulcl  27167  lgsmulsqcoprm  27261  gausslemma2dlem1a  27283  lgsquad2lem2  27303  dchrisum0fmul  27424  dchrisum0lem1  27434  sltres  27581  nocvxminlem  27696  oldlim  27805  madebdayim  27806  madebdaylemlrcut  27817  readdscl  28357  remulscl  28360  ishpg  28693  brcgr  28834  brbtwn2  28839  axcontlem2  28899  uspgredg2v  29158  usgredg2v  29161  usgr2v1e2w  29186  nb3gr2nb  29318  cusgredg  29358  cplgr3v  29369  cusgrop  29372  rusgr1vtx  29523  iswlkg  29548  wlkeq  29569  wlk1walk  29574  uspgr2wlkeq2  29582  uspgr2wlkeqi  29583  cyclnumvtx  29737  crctcshwlkn0lem3  29749  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  wspthneq1eq2  29797  wwlksnextinj  29836  2wlkdlem7  29869  2wlkdlem8  29870  2pthon3v  29880  s3wwlks2on  29893  elwwlks2  29903  elwspths2spth  29904  rusgrnumwwlks  29911  clwlkclwwlklem2a  29934  clwlkclwwlklem3  29937  clwlkclwwlkf1lem2  29941  clwlkclwwlkf1  29946  clwwlknonex2  30045  3wlkdlem3  30097  uhgr3cyclex  30118  cusconngr  30127  eupth0  30150  frgr3v  30211  1to3vfriswmgr  30216  4cycl2v2nb  30225  frgrnbnb  30229  frgrncvvdeq  30245  frgrwopreglem4a  30246  frgrwopreglem5a  30247  frgrwopreglem4  30251  frgrwopreglem5  30257  frgrhash2wsp  30268  numclwwlk1lem2foa  30290  numclwwlk2  30317  blocni  30741  hvsub4  30973  shscli  31253  shscom  31255  spanunsni  31515  spanpr  31516  5oalem2  31591  5oalem3  31592  5oalem5  31594  3oalem1  31598  hoscl  31681  hoadddi  31739  hoadddir  31740  hosub4  31749  lnophsi  31937  hmops  31956  hmopm  31957  adjadd  32029  leop2  32060  leopadd  32068  leopmuli  32069  pjclem4  32135  pj3si  32143  mdslmd1lem2  32262  mdslmd3i  32268  atomli  32318  atcvatlem  32321  chirredlem3  32328  chirredi  32330  atcvat3i  32332  mdsymlem1  32339  mdsymlem5  32343  cdjreui  32368  cdj3i  32377  addltmulALT  32382  hashxpe  32739  domnmuln0rd  33232  mndpluscn  33923  sxbrsigalem5  34286  probfinmeasbALTV  34427  bnj545  34892  bnj546  34893  bnj557  34898  bnj570  34902  bnj594  34909  bnj1001  34956  bnj1118  34981  txpconn  35226  cvmlift2lem10  35306  gonar  35389  lediv2aALT  35671  altopeq12  35957  altxpsspw  35972  funtransport  36026  neibastop1  36354  filnetlem3  36375  lukshef-ax2  36410  arg-ax  36411  nndivsub  36452  bj-nnftht  36736  bj-nnfan  36743  bj-nnfor  36745  copsex2b  37135  isbasisrelowllem1  37350  isbasisrelowllem2  37351  icoreclin  37352  relowlssretop  37358  rdgeqoa  37365  fvineqsnf1  37405  wl-ax11-lem2  37581  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem4  37625  poimirlem26  37647  poimirlem29  37650  poimirlem30  37651  heicant  37656  mblfinlem1  37658  ismblfin  37662  itg2addnclem  37672  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  prdstotbnd  37795  heibor1lem  37810  isdrngo2  37959  divrngidl  38029  pridlc3  38074  linepsubN  39753  pmapsub  39769  elpaddri  39803  paddasslem14  39834  pmapjoin  39853  dvhfvadd  41092  dvhvaddcomN  41097  bcle2d  42174  imacrhmcl  42509  rimco  42513  rmxynorm  42914  monotoddzzfi  42938  acongtr  42974  mpaaeu  43146  oaltublim  43286  omord2lim  43296  cantnftermord  43316  dflim5  43325  omabs2  43328  tfsconcat0i  43341  ofoafo  43352  naddcnff  43358  oaun3lem1  43370  oaun3lem2  43371  pr2cv  43544  brfvrcld2  43688  rfovcnvf1od  44000  ismnushort  44297  nzin  44314  pm10.14  44355  disjrnmpt2  45189  liminfvalxr  45788  etransclem38  46277  cfsetsnfsetf1  47064  tz6.12-afv2  47245  2elfz2melfz  47323  fz0addge0  47324  2ffzoeq  47332  difltmodne  47347  modn0mul  47362  mod2addne  47369  icceuelpartlem  47440  icceuelpart  47441  ich2exprop  47476  sqrtpwpw2p  47543  fmtnoprmfac1lem  47569  fmtnoprmfac1  47570  lighneallem2  47611  divgcdoddALTV  47687  gbowpos  47764  gbowgt5  47767  gboge9  47769  nnsum3primesgbe  47797  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  isuspgrim  47900  clnbgrgrimlem  47937  clnbgrgrim  47938  isgrtri  47946  isubgr3stgrlem4  47972  grlimgrtri  47999  grlictr  48011  gpgedgvtx0  48056  gpgedg2iv  48062  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  pgn4cyclex  48120  isupwlkg  48129  rngcinvALTV  48268  ringcinvALTV  48302  srhmsubcALTV  48317  mapprop  48338  zlmodzxzadd  48350  domnmsuppn0  48361  ply1mulgsumlem2  48380  lincsum  48422  lincsumcl  48424  lincscmcl  48425  isldepslvec2  48478  digexp  48600  rrx2pnecoorneor  48708  rrx2pnedifcoorneorr  48710  rrx2xpref1o  48711  ehl2eudis0lt  48719  rrx2linest  48735  line2x  48747  itsclc0yqsollem2  48756  seppsepf  48921  thincn0eu  49424