Theorem anim12i 614

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 597	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  615  anim1i  616  anim2i  618  anifp  1072  cgsex2g  3476  cgsex4g  3477  spc2egv  3542  spc2ed  3544  uneqin  4230  2reu4lem  4464  2reu4  4465  disjpr2  4658  ssunieq  4887  iuneq1  4951  iuneq2  4954  copsex2t  5440  propeqop  5455  opthhausdorff  5465  opthhausdorff0  5466  iunopeqop  5469  soeq2  5554  opbrop  5722  xpsspw  5758  coeq1  5806  coeq2  5807  cnveq  5822  dmeq  5852  sotri  6084  tz7.7  6343  funun  6538  fununfun  6540  fundif  6541  funprg  6546  funtp  6549  2elresin  6613  funssxp  6690  fssres  6700  f1cof1  6740  foun  6792  f1un  6794  resdif  6795  f1oco  6797  fvun  6924  elfvmptrab1w  6969  elfvmptrab1  6970  fvn0ssdmfun  7020  dff3  7046  exfo  7051  fprg  7102  ftpg  7103  f1ounsn  7220  weisoeq2  7304  oprabv  7420  ndmovdistr  7549  ndmovord  7550  brrpssg  7672  eldifpw  7715  iunpw  7718  epweon  7722  bropfvvvv  8035  f1o2ndf1  8065  poseq  8101  fvn0elsupp  8123  smores  8285  tz7.49  8377  tz7.49c  8378  oaord  8475  oeeulem  8530  nnaord  8548  brecop  8750  brecop2  8751  eroveu  8752  ecopovtrn  8760  ixpeq2  8852  undifixp  8875  sbthlem8  9025  sbthlem9  9026  unxpdom  9162  isinf  9168  f1opwfi  9259  fiin  9328  en2lp  9518  inf3lem3  9542  brttrcl  9625  tcmin  9651  djuexb  9824  alephfp  10021  kmlem16  10079  endjudisj  10082  cofsmo  10182  fin23lem28  10253  axdc3lem2  10364  ac6c4  10394  brdom3  10441  brdom5  10442  brdom4  10443  canthp1lem2  10567  finngch  10569  ordpipq  10856  adderpq  10870  mulerpq  10871  lterpq  10884  genpn0  10917  genpnnp  10919  addclprlem2  10931  addcmpblnr  10983  addsrpr  10989  mulsrpr  10990  addclsr  10997  addasssr  11002  distrsr  11005  0idsr  11011  1idsr  11012  00sr  11013  mulgt0sr  11019  axaddf  11059  axaddass  11070  axdistr  11072  cnegex  11318  recextlem2  11772  difgtsumgt  12481  zaddcl  12558  qaddcl  12906  qmulcl  12908  qreccl  12910  xmulgt0  13226  xrsupsslem  13250  xrinfmsslem  13251  supxrpnf  13261  iccss  13358  difreicc  13428  fzadd2  13504  fzsubel  13505  ssfzunsnext  13514  difelfznle  13587  2ffzeq  13594  nelfzo  13610  fzonmapblen  13654  ubmelfzo  13676  ubmelm1fzo  13709  elfznelfzo  13719  subfzo0  13738  adddivflid  13768  modaddid  13860  modifeq2int  13886  modaddmodup  13887  addmodlteq  13899  fsuppmapnn0fiub  13944  mulexp  14054  mulexpz  14055  leexp1a  14128  faclbnd  14243  hashunx  14339  hashgt23el  14377  wrdeq  14489  ccatcl  14527  swrdnd  14608  swrdnd0  14611  swrdsbslen  14618  swrdspsleq  14619  pfxccat1  14655  swrdswrdlem  14657  pfxccatin12lem2a  14680  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccatin12  14686  swrdccat  14688  reuccatpfxs1  14700  repswswrd  14737  repswccat  14739  cshwidxn  14762  cshweqdif2  14772  2cshwcshw  14778  cshwcshid  14780  cshwcsh2id  14781  f1oun2prg  14870  s2eq2s1eq  14889  s3eqs2s1eq  14891  s3sndisj  14920  s3iunsndisj  14921  sqabsadd  15235  sqabssub  15236  abs2dif  15286  rexanuz  15299  o1of2  15566  o1rlimmul  15572  fsum2dlem  15723  isumltss  15804  fprodser  15905  fprodeq0  15931  fprod2dlem  15936  dvdscmulr  16244  dvdsmulcr  16245  summodnegmod  16246  difmod0  16247  dvds2ln  16249  dvdsflip  16277  divalglem9  16361  gcdcllem3  16461  gcdaddmlem  16484  sqgcd  16522  lcmcllem  16556  lcmabs  16565  lcmgcdlem  16566  lcmgcd  16567  lcmgcdeq  16572  lcmftp  16596  lcmfunsnlem2lem1  16598  qredeq  16617  cncongr1  16627  cncongr2  16628  isprm7  16669  hashgcdlem  16749  dvdsprmpweqle  16848  difsqpwdvds  16849  prmgaplem4  17016  cshwsidrepsw  17055  setsfun0  17133  setsstruct2  17135  xpsfrnel2  17519  isfunc  17822  tsrss  18546  chnpof1  18587  rabsubmgmd  18663  resmgmhm2  18671  mndpfsupp  18726  ismhm0  18749  mhmismgmhm  18750  mndissubm  18766  resmndismnd  18767  resmhm2  18780  submefmnd  18854  sursubmefmnd  18855  injsubmefmnd  18856  grpissubg  19113  gimco  19234  symg2bas  19359  pgrpsubgsymg  19375  symgextf  19383  fvcosymgeq  19395  gsmsymgreqlem1  19396  symgfixf1  19403  efgrelexlema  19715  gsum2dlem1  19936  gsum2dlem2  19937  dvdsr  20333  isrnghmmul  20413  c0ghm  20432  rhmisrnghm  20451  subrngpropd  20536  subrgpropd  20576  rnghmsubcsetclem2  20600  rngcinv  20605  rhmsubcsetclem2  20629  rhmsubcrngclem2  20635  ringcinv  20639  srhmsubc  20648  islmhm2  21025  psgnghm  21570  psgndiflemB  21590  frlmbas3  21766  frlmphl  21771  islindf4  21828  ressmpladd  22017  ressmplmul  22018  mplind  22058  mpomatmul  22421  mavmul0g  22528  1marepvsma1  22558  mdetdiag  22574  slesolvec  22654  cramerimplem2  22659  cramerimplem3  22660  cramerimp  22661  mat2pmatlin  22710  m2pmfzgsumcl  22723  monmatcollpw  22754  pmatcollpw3lem  22758  pmatcollpwscmatlem1  22764  chpmat1dlem  22810  chfacfisf  22829  chfacfisfcpmat  22830  chfacfpmmulgsum2  22840  tgcl  22944  uncld  23016  innei  23100  cnco  23241  uncmp  23378  txbas  23542  txbasval  23581  tx1stc  23625  fbun  23815  infil  23838  fbunfip  23844  filuni  23860  imaelfm  23926  txflf  23981  tsmsfbas  24103  tsmsxp  24130  blin2  24404  nmhmplusg  24732  qtopbaslem  24733  iccntr  24797  ncvspi  25133  ncvs1  25134  unmbl  25514  volfiniun  25524  mbfi1flimlem  25699  ply1idom  26100  logreclem  26739  relogbcxpb  26764  fsumvma2  27191  chpchtsum  27196  dchrelbas3  27215  dchrmulcl  27226  lgsmulsqcoprm  27320  gausslemma2dlem1a  27342  lgsquad2lem2  27362  dchrisum0fmul  27483  dchrisum0lem1  27493  ltsres  27640  nocvxminlem  27760  oldlim  27893  madebdayim  27894  madebdaylemlrcut  27905  readdscl  28505  remulscl  28508  ishpg  28841  brcgr  28983  brbtwn2  28988  axcontlem2  29048  uspgredg2v  29307  usgredg2v  29310  usgr2v1e2w  29335  nb3gr2nb  29467  cusgredg  29507  cplgr3v  29518  cusgrop  29521  rusgr1vtx  29672  iswlkg  29697  wlkeq  29717  wlk1walk  29722  uspgr2wlkeq2  29730  uspgr2wlkeqi  29731  cyclnumvtx  29883  crctcshwlkn0lem3  29895  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  wspthneq1eq2  29943  wwlksnextinj  29982  2wlkdlem7  30015  2wlkdlem8  30016  2pthon3v  30026  s3wwlks2on  30039  sps3wwlks2on  30040  elwwlks2  30052  elwspths2spth  30053  rusgrnumwwlks  30060  clwlkclwwlklem2a  30083  clwlkclwwlklem3  30086  clwlkclwwlkf1lem2  30090  clwlkclwwlkf1  30095  clwwlknonex2  30194  3wlkdlem3  30246  uhgr3cyclex  30267  cusconngr  30276  eupth0  30299  frgr3v  30360  1to3vfriswmgr  30365  4cycl2v2nb  30374  frgrnbnb  30378  frgrncvvdeq  30394  frgrwopreglem4a  30395  frgrwopreglem5a  30396  frgrwopreglem4  30400  frgrwopreglem5  30406  frgrhash2wsp  30417  numclwwlk1lem2foa  30439  numclwwlk2  30466  blocni  30891  hvsub4  31123  shscli  31403  shscom  31405  spanunsni  31665  spanpr  31666  5oalem2  31741  5oalem3  31742  5oalem5  31744  3oalem1  31748  hoscl  31831  hoadddi  31889  hoadddir  31890  hosub4  31899  lnophsi  32087  hmops  32106  hmopm  32107  adjadd  32179  leop2  32210  leopadd  32218  leopmuli  32219  pjclem4  32285  pj3si  32293  mdslmd1lem2  32412  mdslmd3i  32418  atomli  32468  atcvatlem  32471  chirredlem3  32478  chirredi  32480  atcvat3i  32482  mdsymlem1  32489  mdsymlem5  32493  cdjreui  32518  cdj3i  32527  addltmulALT  32532  hashxpe  32895  domnmuln0rd  33350  mndpluscn  34086  sxbrsigalem5  34448  probfinmeasbALTV  34589  bnj545  35053  bnj546  35054  bnj557  35059  bnj570  35063  bnj594  35070  bnj1001  35117  bnj1118  35142  txpconn  35430  cvmlift2lem10  35510  gonar  35593  lediv2aALT  35875  altopeq12  36160  altxpsspw  36175  funtransport  36229  neibastop1  36557  filnetlem3  36578  lukshef-ax2  36613  arg-ax  36614  nndivsub  36655  bj-nnfan  37067  bj-nnfor  37069  cgsex2gd  37467  copsex2b  37470  isbasisrelowllem1  37685  isbasisrelowllem2  37686  icoreclin  37687  relowlssretop  37693  rdgeqoa  37700  fvineqsnf1  37740  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem4  37959  poimirlem26  37981  poimirlem29  37984  poimirlem30  37985  heicant  37990  mblfinlem1  37992  ismblfin  37996  itg2addnclem  38006  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  prdstotbnd  38129  heibor1lem  38144  isdrngo2  38293  divrngidl  38363  pridlc3  38408  eldisjdmqsim  39152  linepsubN  40212  pmapsub  40228  elpaddri  40262  paddasslem14  40293  pmapjoin  40312  dvhfvadd  41551  dvhvaddcomN  41556  bcle2d  42632  imacrhmcl  42973  rimco  42977  rmxynorm  43364  monotoddzzfi  43388  acongtr  43424  mpaaeu  43596  oaltublim  43736  omord2lim  43746  cantnftermord  43766  dflim5  43775  omabs2  43778  tfsconcat0i  43791  ofoafo  43802  naddcnff  43808  oaun3lem1  43820  oaun3lem2  43821  pr2cv  43993  brfvrcld2  44137  rfovcnvf1od  44449  ismnushort  44746  nzin  44763  pm10.14  44804  disjrnmpt2  45636  liminfvalxr  46229  etransclem38  46718  cfsetsnfsetf1  47519  tz6.12-afv2  47700  2elfz2melfz  47778  fz0addge0  47779  2ffzoeq  47788  difltmodne  47808  modn0mul  47823  mod2addne  47830  icceuelpartlem  47907  icceuelpart  47908  ich2exprop  47943  sqrtpwpw2p  48013  fmtnoprmfac1lem  48039  fmtnoprmfac1  48040  lighneallem2  48081  divgcdoddALTV  48170  gbowpos  48247  gbowgt5  48250  gboge9  48252  nnsum3primesgbe  48280  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  isuspgrim  48384  clnbgrgrimlem  48421  clnbgrgrim  48422  isgrtri  48431  isubgr3stgrlem4  48457  grlimgrtri  48491  grlictr  48503  gpgedgvtx0  48549  gpgedg2iv  48555  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612  pgn4cyclex  48614  isupwlkg  48625  rngcinvALTV  48764  ringcinvALTV  48798  srhmsubcALTV  48813  mapprop  48834  zlmodzxzadd  48846  domnmsuppn0  48857  ply1mulgsumlem2  48875  lincsum  48917  lincsumcl  48919  lincscmcl  48920  isldepslvec2  48973  digexp  49095  rrx2pnecoorneor  49203  rrx2pnedifcoorneorr  49205  rrx2xpref1o  49206  ehl2eudis0lt  49214  rrx2linest  49230  line2x  49242  itsclc0yqsollem2  49251  seppsepf  49416  thincn0eu  49918