Theorem anim12i 590

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  anim12ci  591  anim1i  592  anim2i  593  anifp  1020  sbimi  1886  cgsex2g  3239  cgsex4g  3240  spc2egv  3295  sseq2  3627  uneqin  3878  undif3OLD  3889  disjpr2  4248  ssunieq  4472  iuneq1  4534  iuneq2  4537  copsex2t  4957  propeqop  4970  iunopeqop  4981  soeq2  5055  opbrop  5198  xpsspw  5233  coeq1  5279  coeq2  5280  cnveq  5296  dmeq  5324  sotri  5523  tz7.7  5749  funun  5932  fununfun  5934  fundif  5935  funprg  5940  funtp  5945  funcnvqpOLD  5953  2elresin  6002  funssxp  6061  fssres  6070  f1co  6110  foun  6155  resdif  6157  f1oco  6159  fvun  6268  elfvmptrab1  6305  fvn0ssdmfun  6350  dff3  6372  exfo  6377  fprg  6422  ftpg  6423  weisoeq2  6606  oprabv  6703  ndmovdistr  6823  ndmovord  6824  brrpssg  6939  eldifpw  6976  iunpw  6978  bropfvvvv  7257  f1o2ndf1  7285  fvn0elsupp  7311  wfrlem5  7419  smores  7449  tz7.49  7540  tz7.49c  7541  oaord  7627  oeeulem  7681  nnaord  7699  brecop  7840  brecop2  7841  eroveu  7842  ecopovtrn  7850  ixpeq2  7922  undifixp  7944  undom  8048  sbthlem8  8077  sbthlem9  8078  unxpdom  8167  isinf  8173  f1opwfi  8270  fiin  8328  en2lp  8510  inf3lem3  8527  tcmin  8617  alephfp  8931  kmlem16  8987  cdaval  8992  cdaun  8994  cofsmo  9091  fin23lem28  9162  axdc3lem2  9273  ac6c4  9303  brdom3  9350  brdom5  9351  brdom4  9352  canthp1lem2  9475  finngch  9477  ordpipq  9764  adderpq  9778  mulerpq  9779  lterpq  9792  genpn0  9825  genpnnp  9827  addclprlem2  9839  addcmpblnr  9890  addsrpr  9896  mulsrpr  9897  addclsr  9904  addasssr  9909  distrsr  9912  0idsr  9918  1idsr  9919  00sr  9920  mulgt0sr  9926  axaddf  9966  axaddass  9977  axdistr  9979  cnegex  10217  recextlem2  10658  difgtsumgt  11346  zaddcl  11417  qaddcl  11804  qmulcl  11806  qreccl  11808  xmulgt0  12113  xrsupsslem  12137  xrinfmsslem  12138  supxrpnf  12148  iccss  12241  difreicc  12304  fzadd2  12376  fzsubel  12377  ssfzunsnext  12386  elfz0add  12438  difelfznle  12453  2ffzeq  12460  nelfzo  12475  fzonmapblen  12513  ubmelfzo  12532  ubmelm1fzo  12564  elfznelfzo  12573  subfzo0  12590  adddivflid  12619  modifeq2int  12732  modaddmodup  12733  addmodlteq  12745  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  mulexp  12899  mulexpz  12900  leexp1a  12919  faclbnd  13077  hashunx  13175  wrdeq  13327  ccatcl  13359  swrdnd  13432  swrdeq  13444  swrdsbslen  13448  swrdspsleq  13449  swrdswrdlem  13459  reuccats1  13480  swrdccatin12lem2a  13485  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12  13491  swrdccat  13493  repswswrd  13531  repswccat  13532  cshwidxn  13555  cshweqdif2  13565  2cshwcshw  13571  cshwcshid  13573  cshwcsh2id  13574  f1oun2prg  13662  s2eq2s1eq  13681  s3eqs2s1eq  13683  wwlktovf1  13700  s3sndisj  13706  s3iunsndisj  13707  sqabsadd  14022  sqabssub  14023  abs2dif  14072  rexanuz  14085  o1of2  14343  o1rlimmul  14349  fsum2dlem  14501  isumltss  14580  fprodser  14679  fprodeq0  14705  fprod2dlem  14710  dvdscmulr  15010  dvdsmulcr  15011  summodnegmod  15012  dvds2ln  15014  dvdsflip  15039  divalglem9  15124  gcdcllem3  15223  gcdaddmlem  15245  gcdabs  15250  sqgcd  15278  lcmcllem  15309  lcmabs  15318  lcmgcdlem  15319  lcmgcd  15320  lcmgcdeq  15325  lcmf  15346  lcmftp  15349  lcmfunsnlem2lem1  15351  qredeq  15371  cncongr1  15381  cncongr2  15382  isprm7  15420  hashgcdlem  15493  pythagtriplem19  15538  dvdsprmpweqle  15590  difsqpwdvds  15591  prmgaplem4  15758  cshwsidrepsw  15800  setsfun0  15894  setsstruct2  15896  setsstructOLD  15899  xpsfrnel2  16225  isfunc  16524  fpwipodrs  17164  tsrss  17223  resmhm2  17360  gimco  17710  symg2bas  17818  pgrpsubgsymg  17828  symgextf  17837  gsmsymgrfixlem1  17847  fvcosymgeq  17849  gsmsymgreqlem1  17850  symgfixf1  17857  efgrelexlema  18162  gsum2dlem1  18369  gsum2dlem2  18370  dvdsr  18646  subrgpropd  18814  islmhm2  19038  ressmpladd  19457  ressmplmul  19458  mplind  19502  psgnghm  19926  psgndiflemB  19946  frlmbas3  20115  frlmphl  20120  islindf4  20177  mpt2matmul  20252  mavmul0g  20359  1marepvsma1  20389  mdetdiag  20405  slesolvec  20485  cramerimplem2  20490  cramerimplem3  20491  cramerimp  20492  mat2pmatlin  20540  m2pmfzgsumcl  20553  monmatcollpw  20584  pmatcollpw3lem  20588  pmatcollpwscmatlem1  20594  chpmat1dlem  20640  chfacfisf  20659  chfacfisfcpmat  20660  chfacfpmmulgsum2  20670  tgcl  20773  uncld  20845  innei  20929  cnco  21070  uncmp  21206  txbas  21370  txbasval  21409  tx1stc  21453  fbun  21644  infil  21667  fbunfip  21673  filuni  21689  imaelfm  21755  txflf  21810  tsmsfbas  21931  tsmsxp  21958  blin2  22234  nmhmplusg  22561  qtopbaslem  22562  iccntr  22624  ncvspi  22956  ncvs1  22957  unmbl  23305  volfiniun  23315  mbfi1flimlem  23489  ply1idom  23884  logreclem  24500  relogbcxpb  24525  fsumvma2  24939  chpchtsum  24944  dchrelbas3  24963  dchrmulcl  24974  lgsmulsqcoprm  25068  gausslemma2dlem1a  25090  lgsquad2lem2  25110  dchrisum0fmul  25195  dchrisum0lem1  25205  ishpg  25651  brcgr  25780  brbtwn2  25785  axcontlem2  25845  uspgredg2v  26116  usgredg2v  26119  usgr2v1e2w  26144  nb3gr2nb  26286  cusgredg  26320  cplgr3v  26331  cusgrop  26334  rusgr1vtx  26484  iswlkg  26509  wlkeq  26529  wlk1walk  26535  uspgr2wlkeq2  26543  uspgr2wlkeqi  26544  crctcshwlkn0lem3  26704  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  wspthneq1eq2  26745  wlkwwlkfun  26781  wwlksnextinj  26794  2wlkdlem7  26828  2wlkdlem8  26829  2pthon3v  26839  s3wwlks2on  26849  elwwlks2  26861  elwspths2spth  26862  rusgrnumwwlks  26869  clwwlknp  26887  clwlkclwwlklem2a  26899  clwlkclwwlklem3  26902  clwlksf1clwwlk  26969  3wlkdlem3  27021  uhgr3cyclex  27042  cusconngr  27051  eupth0  27074  frgr3v  27139  1to3vfriswmgr  27144  4cycl2v2nb  27153  frgrnbnb  27157  frgrncvvdeq  27173  frgrwopreglem4a  27174  frgrwopreglem5a  27175  frgrwopreglem4  27179  frgrwopreglem5  27185  frgrhash2wsp  27196  numclwwlkovf2ex  27219  numclwlk1lem2fo  27228  numclwwlk2lem1  27235  numclwwlk2  27240  blocni  27660  hvsub4  27894  shscli  28176  shscom  28178  spanunsni  28438  spanpr  28439  5oalem2  28514  5oalem3  28515  5oalem5  28517  3oalem1  28521  hoscl  28604  hoadddi  28662  hoadddir  28663  hosub4  28672  lnophsi  28860  hmops  28879  hmopm  28880  adjadd  28952  leop2  28983  leopadd  28991  leopmuli  28992  pjclem4  29058  pj3si  29066  mdslmd1lem2  29185  mdslmd3i  29191  atomli  29241  atcvatlem  29244  chirredlem3  29251  chirredi  29253  atcvat3i  29255  mdsymlem1  29262  mdsymlem5  29266  cdjreui  29291  cdj3i  29300  addltmulALT  29305  spc2ed  29312  mndpluscn  29972  sxbrsigalem5  30350  probfinmeasbOLD  30490  bnj545  30965  bnj546  30966  bnj557  30971  bnj570  30975  bnj594  30982  bnj1001  31028  bnj1118  31052  txpconn  31214  cvmlift2lem10  31294  lediv2aALT  31571  poseq  31750  frrlem5  31784  sltres  31815  nocvxminlem  31893  sslttr  31914  altopeq12  32069  altxpsspw  32084  funtransport  32138  neibastop1  32354  filnetlem3  32375  lukshef-ax2  32414  arg-ax  32415  nndivsub  32456  isbasisrelowllem1  33203  isbasisrelowllem2  33204  icoreclin  33205  relowlssretop  33211  rdgeqoa  33218  wl-ax11-lem2  33363  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem4  33413  poimirlem26  33435  poimirlem29  33438  poimirlem30  33439  heicant  33444  mblfinlem1  33446  ismblfin  33450  itg2addnclem  33461  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  prdstotbnd  33593  heibor1lem  33608  isdrngo2  33757  divrngidl  33827  pridlc3  33872  linepsubN  35038  pmapsub  35054  elpaddri  35088  paddasslem14  35119  pmapjoin  35138  dvhfvadd  36380  dvhvaddcomN  36385  rmxynorm  37483  monotoddzzfi  37507  acongtr  37545  mpaaeu  37720  brfvrcld2  37984  rfovcnvf1od  38298  nzin  38517  pm10.14  38558  liminfvalxr  40015  etransclem38  40489  2reu4a  41189  2reu4  41190  2elfz2melfz  41328  fz0addge0  41329  2ffzoeq  41338  icceuelpartlem  41371  icceuelpart  41372  pfxeq  41404  pfxsuffeqwrdeq  41406  pfxccat1  41410  pfxccatin12lem2  41424  pfxccatin12  41425  sqrtpwpw2p  41450  fmtnoprmfac1lem  41476  fmtnoprmfac1  41477  lighneallem2  41523  divgcdoddALTV  41593  gbowpos  41647  gbowgt5  41650  gboge9  41652  nnsum3primesgbe  41680  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  isupwlkg  41718  rabsubmgmd  41791  resmgmhm2  41799  ismhm0  41805  mhmismgmhm  41806  isrnghmmul  41893  c0ghm  41911  rhmisrnghm  41920  rnghmsubcsetclem2  41976  rngcinv  41981  rngcinvALTV  41993  rhmsubcsetclem2  42022  rhmsubcrngclem2  42028  ringcinv  42032  ringcinvALTV  42056  srhmsubc  42076  srhmsubcALTV  42094  mapprop  42124  zlmodzxzadd  42136  domnmsuppn0  42150  mndpfsupp  42157  ply1mulgsumlem2  42175  lincsum  42218  lincsumcl  42220  lincscmcl  42221  isldepslvec2  42274  modn0mul  42315  digexp  42401