Theorem anim12i 616

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anim12ci  617  anim1i  618  anim2i  620  anifp  1072  norassOLD  1540  cgsex2g  3441  cgsex4g  3442  cgsex4gOLD  3443  spc2egv  3504  spc2ed  3506  sseq2  3913  uneqin  4179  2reu4lem  4423  2reu4  4424  disjpr2  4615  ssunieq  4842  iuneq1  4906  iuneq2  4909  copsex2t  5360  propeqop  5375  opthhausdorff  5385  opthhausdorff0  5386  iunopeqop  5389  soeq2  5475  opbrop  5630  xpsspw  5664  coeq1  5711  coeq2  5712  cnveq  5727  dmeq  5757  sotri  5972  tz7.7  6217  funun  6404  fununfun  6406  fundif  6407  funprg  6412  funtp  6415  2elresin  6476  funssxp  6552  fssres  6563  f1cof1  6604  f1coOLD  6606  foun  6657  resdif  6659  f1oco  6661  fvun  6779  elfvmptrab1w  6822  elfvmptrab1  6823  fvn0ssdmfun  6873  dff3  6897  exfo  6902  fprg  6948  ftpg  6949  weisoeq2  7143  oprabv  7249  ndmovdistr  7375  ndmovord  7376  brrpssg  7491  eldifpw  7531  iunpw  7534  bropfvvvv  7838  f1o2ndf1  7869  fvn0elsupp  7900  wfrlem5  8037  smores  8067  tz7.49  8159  tz7.49c  8160  oaord  8253  oeeulem  8307  nnaord  8325  brecop  8470  brecop2  8471  eroveu  8472  ecopovtrn  8480  ixpeq2  8570  undifixp  8593  undom  8711  sbthlem8  8741  sbthlem9  8742  unxpdom  8861  isinf  8867  f1opwfi  8958  fiin  9016  en2lp  9199  inf3lem3  9223  tcmin  9335  djuexb  9490  alephfp  9687  kmlem16  9744  endjudisj  9747  cofsmo  9848  fin23lem28  9919  axdc3lem2  10030  ac6c4  10060  brdom3  10107  brdom5  10108  brdom4  10109  canthp1lem2  10232  finngch  10234  ordpipq  10521  adderpq  10535  mulerpq  10536  lterpq  10549  genpn0  10582  genpnnp  10584  addclprlem2  10596  addcmpblnr  10648  addsrpr  10654  mulsrpr  10655  addclsr  10662  addasssr  10667  distrsr  10670  0idsr  10676  1idsr  10677  00sr  10678  mulgt0sr  10684  axaddf  10724  axaddass  10735  axdistr  10737  cnegex  10978  recextlem2  11428  difgtsumgt  12108  zaddcl  12182  qaddcl  12526  qmulcl  12528  qreccl  12530  xmulgt0  12838  xrsupsslem  12862  xrinfmsslem  12863  supxrpnf  12873  iccss  12968  difreicc  13037  fzadd2  13112  fzsubel  13113  ssfzunsnext  13122  difelfznle  13191  2ffzeq  13198  nelfzo  13213  fzonmapblen  13253  ubmelfzo  13272  ubmelm1fzo  13303  elfznelfzo  13312  subfzo0  13329  adddivflid  13358  modifeq2int  13471  modaddmodup  13472  addmodlteq  13484  fsuppmapnn0fiub  13529  mulexp  13639  mulexpz  13640  leexp1a  13710  faclbnd  13821  hashunx  13918  hashgt23el  13956  wrdeq  14056  ccatcl  14094  swrdnd  14184  swrdnd0  14187  swrdsbslen  14194  swrdspsleq  14195  pfxccat1  14232  swrdswrdlem  14234  pfxccatin12lem2a  14257  swrdccatin2  14259  pfxccatin12lem2  14261  pfxccatin12  14263  swrdccat  14265  reuccatpfxs1  14277  repswswrd  14314  repswccat  14316  cshwidxn  14339  cshweqdif2  14349  2cshwcshw  14355  cshwcshid  14357  cshwcsh2id  14358  f1oun2prg  14447  s2eq2s1eq  14466  s3eqs2s1eq  14468  s3sndisj  14495  s3iunsndisj  14496  sqabsadd  14811  sqabssub  14812  abs2dif  14861  rexanuz  14874  o1of2  15139  o1rlimmul  15145  fsum2dlem  15297  isumltss  15375  fprodser  15474  fprodeq0  15500  fprod2dlem  15505  dvdscmulr  15809  dvdsmulcr  15810  summodnegmod  15811  dvds2ln  15813  dvdsflip  15841  divalglem9  15925  gcdcllem3  16023  gcdaddmlem  16046  gcdabsOLD  16054  sqgcd  16085  lcmcllem  16116  lcmabs  16125  lcmgcdlem  16126  lcmgcd  16127  lcmgcdeq  16132  lcmftp  16156  lcmfunsnlem2lem1  16158  qredeq  16177  cncongr1  16187  cncongr2  16188  isprm7  16228  hashgcdlem  16304  dvdsprmpweqle  16402  difsqpwdvds  16403  prmgaplem4  16570  cshwsidrepsw  16610  setsfun0  16701  setsstruct2  16703  xpsfrnel2  17023  isfunc  17324  tsrss  18049  mndissubm  18188  resmndismnd  18189  resmhm2  18202  submefmnd  18276  sursubmefmnd  18277  injsubmefmnd  18278  grpissubg  18517  gimco  18626  symg2bas  18739  pgrpsubgsymg  18755  symgextf  18763  fvcosymgeq  18775  gsmsymgreqlem1  18776  symgfixf1  18783  efgrelexlema  19093  gsum2dlem1  19309  gsum2dlem2  19310  dvdsr  19618  subrgpropd  19789  islmhm2  20029  psgnghm  20496  psgndiflemB  20516  frlmbas3  20692  frlmphl  20697  islindf4  20754  ressmpladd  20940  ressmplmul  20941  mplind  20982  mpomatmul  21297  mavmul0g  21404  1marepvsma1  21434  mdetdiag  21450  slesolvec  21530  cramerimplem2  21535  cramerimplem3  21536  cramerimp  21537  mat2pmatlin  21586  m2pmfzgsumcl  21599  monmatcollpw  21630  pmatcollpw3lem  21634  pmatcollpwscmatlem1  21640  chpmat1dlem  21686  chfacfisf  21705  chfacfisfcpmat  21706  chfacfpmmulgsum2  21716  tgcl  21820  uncld  21892  innei  21976  cnco  22117  uncmp  22254  txbas  22418  txbasval  22457  tx1stc  22501  fbun  22691  infil  22714  fbunfip  22720  filuni  22736  imaelfm  22802  txflf  22857  tsmsfbas  22979  tsmsxp  23006  blin2  23281  nmhmplusg  23609  qtopbaslem  23610  iccntr  23672  ncvspi  24007  ncvs1  24008  unmbl  24388  volfiniun  24398  mbfi1flimlem  24574  ply1idom  24976  logreclem  25599  relogbcxpb  25624  fsumvma2  26049  chpchtsum  26054  dchrelbas3  26073  dchrmulcl  26084  lgsmulsqcoprm  26178  gausslemma2dlem1a  26200  lgsquad2lem2  26220  dchrisum0fmul  26341  dchrisum0lem1  26351  ishpg  26804  brcgr  26945  brbtwn2  26950  axcontlem2  27010  uspgredg2v  27266  usgredg2v  27269  usgr2v1e2w  27294  nb3gr2nb  27426  cusgredg  27466  cplgr3v  27477  cusgrop  27480  rusgr1vtx  27630  iswlkg  27655  wlkeq  27675  wlk1walk  27680  uspgr2wlkeq2  27688  uspgr2wlkeqi  27689  crctcshwlkn0lem3  27850  crctcshwlkn0lem4  27851  crctcshwlkn0lem5  27852  wspthneq1eq2  27898  wwlksnextinj  27937  2wlkdlem7  27970  2wlkdlem8  27971  2pthon3v  27981  s3wwlks2on  27994  elwwlks2  28004  elwspths2spth  28005  rusgrnumwwlks  28012  clwlkclwwlklem2a  28035  clwlkclwwlklem3  28038  clwlkclwwlkf1lem2  28042  clwlkclwwlkf1  28047  clwwlknonex2  28146  3wlkdlem3  28198  uhgr3cyclex  28219  cusconngr  28228  eupth0  28251  frgr3v  28312  1to3vfriswmgr  28317  4cycl2v2nb  28326  frgrnbnb  28330  frgrncvvdeq  28346  frgrwopreglem4a  28347  frgrwopreglem5a  28348  frgrwopreglem4  28352  frgrwopreglem5  28358  frgrhash2wsp  28369  numclwwlk1lem2foa  28391  numclwwlk2  28418  blocni  28840  hvsub4  29072  shscli  29352  shscom  29354  spanunsni  29614  spanpr  29615  5oalem2  29690  5oalem3  29691  5oalem5  29693  3oalem1  29697  hoscl  29780  hoadddi  29838  hoadddir  29839  hosub4  29848  lnophsi  30036  hmops  30055  hmopm  30056  adjadd  30128  leop2  30159  leopadd  30167  leopmuli  30168  pjclem4  30234  pj3si  30242  mdslmd1lem2  30361  mdslmd3i  30367  atomli  30417  atcvatlem  30420  chirredlem3  30427  chirredi  30429  atcvat3i  30431  mdsymlem1  30438  mdsymlem5  30442  cdjreui  30467  cdj3i  30476  addltmulALT  30481  hashxpe  30801  mndpluscn  31544  sxbrsigalem5  31921  probfinmeasbALTV  32062  bnj545  32542  bnj546  32543  bnj557  32548  bnj570  32552  bnj594  32559  bnj1001  32606  bnj1118  32631  txpconn  32861  cvmlift2lem10  32941  gonar  33024  lediv2aALT  33302  poseq  33482  sltres  33551  nocvxminlem  33658  oldlim  33755  madebdayim  33756  madebdaylemlrcut  33765  altopeq12  33950  altxpsspw  33965  funtransport  34019  neibastop1  34234  filnetlem3  34255  lukshef-ax2  34290  arg-ax  34291  nndivsub  34332  bj-nnftht  34609  bj-nnfan  34616  bj-nnfor  34618  copsex2b  34995  isbasisrelowllem1  35212  isbasisrelowllem2  35213  icoreclin  35214  relowlssretop  35220  rdgeqoa  35227  fvineqsnf1  35267  wl-ax11-lem2  35423  matunitlindflem1  35459  matunitlindflem2  35460  poimirlem4  35467  poimirlem26  35489  poimirlem29  35492  poimirlem30  35493  heicant  35498  mblfinlem1  35500  ismblfin  35504  itg2addnclem  35514  ftc1anclem6  35541  ftc1anclem7  35542  ftc1anclem8  35543  ftc1anc  35544  prdstotbnd  35638  heibor1lem  35653  isdrngo2  35802  divrngidl  35872  pridlc3  35917  linepsubN  37452  pmapsub  37468  elpaddri  37502  paddasslem14  37533  pmapjoin  37552  dvhfvadd  38791  dvhvaddcomN  38796  andiff  39822  rmxynorm  40384  monotoddzzfi  40408  acongtr  40444  mpaaeu  40619  pr2cv  40772  brfvrcld2  40918  rfovcnvf1od  41230  ismnushort  41533  nzin  41550  pm10.14  41591  disjrnmpt2  42340  liminfvalxr  42942  etransclem38  43431  cfsetsnfsetf1  44168  tz6.12-afv2  44347  2elfz2melfz  44426  fz0addge0  44427  2ffzoeq  44436  icceuelpartlem  44503  icceuelpart  44504  ich2exprop  44539  sqrtpwpw2p  44606  fmtnoprmfac1lem  44632  fmtnoprmfac1  44633  lighneallem2  44674  divgcdoddALTV  44750  gbowpos  44827  gbowgt5  44830  gboge9  44832  nnsum3primesgbe  44860  bgoldbtbndlem2  44874  bgoldbtbndlem3  44875  isupwlkg  44915  rabsubmgmd  44961  resmgmhm2  44969  ismhm0  44975  mhmismgmhm  44976  isrnghmmul  45067  c0ghm  45085  rhmisrnghm  45094  rnghmsubcsetclem2  45150  rngcinv  45155  rngcinvALTV  45167  rhmsubcsetclem2  45196  rhmsubcrngclem2  45202  ringcinv  45206  ringcinvALTV  45230  srhmsubc  45250  srhmsubcALTV  45268  mapprop  45298  zlmodzxzadd  45310  domnmsuppn0  45321  mndpfsupp  45328  ply1mulgsumlem2  45344  lincsum  45386  lincsumcl  45388  lincscmcl  45389  isldepslvec2  45442  modn0mul  45482  digexp  45569  rrx2pnecoorneor  45677  rrx2pnedifcoorneorr  45679  rrx2xpref1o  45680  ehl2eudis0lt  45688  rrx2linest  45704  line2x  45716  itsclc0yqsollem2  45725  seppsepf  45838  thincn0eu  45929