Theorem anim1i 626

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
anim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
anim1i	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Proof of Theorem anim1i

Step	Hyp	Ref	Expression
1		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
2		id 23	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	anim12i 624	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  sylanl1  692  sylanr1  694  eu6im  2603  r19.28v  3196  rmob  3844  eqeuel  4321  preq12nebg  4829  fores  6804  fdmeu  6939  ssimaex  6968  dffv2  6978  exfo  7102  fpropnf1  7267  f1ocoima  7303  oprabv  7472  ndmovass  7600  fun11uni  7931  resf1ext2b  7933  f1iun  7942  soxp  8126  tz7.48lem  8429  tz7.49c  8434  omass  8566  oewordri  8579  omabs  8638  sbthlem9  9084  pssnn  9154  fineqvlem  9227  domunfican  9282  fiint  9287  fsuppsssupp  9342  sup0  9428  inf1  9592  infeq5  9607  cantnfle  9641  rankuni  9836  djuunxp  9908  acndom  10036  acnnum  10037  cdainflem  10172  cfcof  10259  ac6num  10464  ac6s2  10471  brdom5  10514  brdom4  10515  genpnnp  10991  divmulasscom  11897  lediv2a  12110  supmul1  12185  infregelb  12200  nn2ge  12264  btwnz  12700  eluz2b2  12946  uz2mulcl  12951  eqreznegel  12959  xrsupexmnf  13332  xrinfmexpnf  13333  xrsupsslem  13334  xrinfmsslem  13335  supxrun  13343  ioo0  13398  elioo4g  13434  fz0fzelfz0  13664  fz0fzdiffz0  13667  2ffzeq  13679  elfzodifsumelfzo  13762  elfzom1elp1fzo  13763  zpnn0elfzo  13769  elfzom1elp1fzo1  13798  fzonfzoufzol  13802  quoremnn0  13891  zmodidfzoimp  13936  modabs  13939  modaddb  13944  modifeq2int  13971  modaddmulmod  13976  expcl2lem  14111  hashgt23el  14463  hashreshashfun  14478  iswrdsymb  14570  ccatcl  14613  ccatsymb  14622  swrdfv2  14701  swrdsbslen  14704  swrdspsleq  14705  pfxswrd  14745  pfxccatin12lem3  14771  pfxccatpfx2  14776  swrdccat3blem  14778  reuccatpfxs1  14786  repswccat  14825  cshweqdifid  14859  lswco  14878  repsco  14879  s4f1o  14957  trclun  15053  mulre  15174  rediv  15184  imdiv  15191  resqrex  15303  caurcvg2  15731  fsumdifsnconst  15845  modfsummods  15847  tanval  16185  p1modz1  16318  negdvdsb  16331  muldvds1  16339  muldvds2  16340  dvdscmulr  16343  dvdsmulcr  16344  sumodd  16447  divalglem8  16459  divgcdnn  16574  lcmfunsnlem2lem2  16698  lcmfun  16704  2mulprm  16752  maxprmfct  16769  vfermltlALT  16863  modprm0  16866  pcpremul  16904  pcmul  16912  oddprmdvds  16964  prmdvdsprmo  17103  cshwsidrepsw  17154  gsumccat  18901  grpissubg  19214  ecqusaddd  19264  ecqusaddcl  19265  eqg0subg  19268  gim0to0  19340  gsmsymgreqlem2  19502  symgfixfo  19510  fsfnn0gsumfsffz  20054  rnglz  20244  isringrng  20371  irredn0  20506  c0snmgmhm  20545  rimisrngim  20581  zrrnghm  20622  rnghmsubcsetclem2  20718  rhmsubcsetclem2  20747  rhmsubcrngclem2  20753  lsppratlem1  21252  qusmulrng  21403  quscrng  21404  rngqiprngghmlem3  21410  rngqiprnglinlem3  21414  rngqiprngimf1lem  21415  rngqiprnglin  21423  cnfldfunALT  21518  dvdsrzring  21592  mpofrlmd  21908  matinvgcell  22573  mat1dimcrng  22615  dmatscmcl  22641  scmatscm  22651  scmatghm  22671  scmatmhm  22672  ma1repvcl  22708  slesolinv  22818  slesolinvbi  22819  cramerimplem1  22821  cramerimp  22824  cramerlem1  22825  cramer  22829  cpmatacl  22854  cpmatmcl  22857  mat2pmatghm  22868  mat2pmatmul  22869  m2pmfzgsumcl  22886  decpmatmul  22910  decpmatmulsumfsupp  22911  pmatcollpwfi  22920  pm2mpf1  22937  pm2mpghm  22954  pm2mpmhmlem1  22956  monmat2matmon  22962  chpdmatlem2  22977  chpdmat  22979  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  clscld  23185  neiptopnei  23270  2ndcdisj2  23595  comppfsc  23670  tx1stc  23788  opnfbas  23980  fbasfip  24006  alexsublem  24182  alexsubALTlem4  24188  cnextcn  24205  ngpocelbl  24842  cphipval  25383  bcthlem5  25468  vitalilem4  25751  vitalilem5  25752  itg2mulc  25887  bddiblnc  25982  dvcobr  26086  dvcnvlem  26116  dvferm1  26125  dvne0  26151  mdegmullem  26216  plyeq0lem  26348  plyexmo  26455  aalioulem5  26478  aalioulem6  26479  aaliou  26480  cxple2a  26842  cxpaddlelem  26894  cxpaddle  26895  relogbcxpb  26930  bcmono  27419  lgsprme0  27481  gausslemma2dlem0e  27502  gausslemma2dlem1a  27507  gausslemma2dlem6  27514  lgsquadlem2  27523  2lgsoddprm  27558  elno2  27796  cofcutr  28095  colinearalg  29238  axcontlem3  29294  umgrislfupgrlem  29450  edgupgr  29462  usgruspgrb  29511  usgrislfuspgr  29515  edgssv2  29526  umgr2edg  29537  uspgredg2v  29552  usgrexmplef  29587  subupgr  29615  subusgr  29617  nbupgrres  29692  nb3gr2nb  29712  nbupgruvtxres  29735  cusgrres  29776  cusgrsizeindslem  29779  cusgrsizeinds  29780  vtxdun  29809  finrusgrfusgr  29893  cusgrrusgr  29909  pthdifv  30057  spthdep  30061  cycliscrct  30126  crctcshwlkn0lem6  30142  crctcshwlkn0lem7  30143  crctcshtrl  30150  crctcsh  30151  umgr2adedgwlkonALT  30274  elwwlks2  30296  elwspths2spth  30297  rusgrnumwwlk  30305  clwlkclwwlklem2a  30327  clwlkclwwlklem3  30330  clwwisshclwws  30344  wwlksubclwwlk  30387  eleclclwwlknlem2  30390  eupth2lem3lem3  30559  eucrct2eupth1  30573  frgr3v  30604  3vfriswmgr  30607  1to3vfriswmgr  30609  3cyclfrgr  30617  vdgn1frgrv2  30625  frgrwopreglem5  30650  frgrwopreglem5ALT  30651  frrusgrord0lem  30668  frrusgrord0  30669  2clwwlk2clwwlk  30679  extwwlkfab  30681  numclwwlk1lem2fo  30687  friendshipgt3  30727  ex-natded9.20-2  30747  grpoidinvlem3  30836  grpoidinv  30838  nmobndseqi  31109  nmobndseqiALT  31110  hvaddsub4  31408  ocsh  31613  5oalem2  31985  5oalem5  31988  3oalem2  31993  pjjsi  32030  hoadddir  32134  leopmul  32464  stge1i  32568  hatomistici  32692  mdsymlem2  32734  mdsymlem5  32737  addltmulALT  32776  isoun  33025  fsumiunle  33151  lsmsnorb  33682  crefdf  34216  qqhre  34388  esumiun  34462  sxbrsigalem0  34639  dya2iocnei  34650  sxbrsigalem5  34656  sibfinima  34707  eulerpartlemgs2  34748  ballotlemfc0  34861  ballotlemfcc  34862  ballotlemsup  34873  bnj529  35108  bnj945  35140  bnj1098  35150  bnj1533  35218  bnj605  35273  bnj594  35278  bnj607  35282  bnj966  35310  bnj967  35311  bnj996  35322  bnj999  35324  bnj1006  35326  bnj1118  35350  bnj1172  35367  bnj1279  35384  bnj1296  35387  bnj1498  35427  fnrelpredd  35460  lfuhgr3  35590  loop1cycl  35607  cvmsi  35735  satf0op  35847  satffunlem1lem1  35872  satffunlem2lem1  35874  fv2ndcnv  36248  trisegint  36498  funtransport  36501  btwnconn1lem4  36560  btwnconn2  36572  segcon2  36575  outsideofeu  36601  isfne  36828  lukshef-ax2  36904  limsucncmpi  36934  weiunso  36955  bj-nsnid  37684  bj-restn0b  37711  bj-eldiag2  37799  bj-isrvec2  37922  pibt2  38041  unccur  38232  lindsadd  38242  lindsenlbs  38244  matunitlindflem1  38245  matunitlindflem2  38246  poimirlem26  38275  poimirlem27  38276  poimirlem29  38278  poimirlem30  38279  poimirlem32  38281  heicant  38284  ismblfin  38290  itg2gt0cn  38304  areacirc  38342  opelopab3  38347  isdivrngo  38579  isdrngo2  38587  fldcrngo  38633  flddmn  38687  refrelredund4  39346  mainer2  39587  cmtbr4N  40007  linepsubN  40504  pmapsub  40520  paddasslem14  40585  pclcmpatN  40653  trlval2  40915  cdleme20  41076  cdleme21j  41088  dvalveclem  41777  dia2dimlem7  41822  dvhlveclem  41860  docaclN  41876  dihjat1  42181  mapdhcl  42479  mapdh6dN  42491  mapdh8  42540  hdmap1l6d  42565  hdmap10  42592  hdmaprnlem17N  42615  hdmaplkr  42665  hdmapip0  42667  hgmapvv  42678  aks6d1c4  42869  cmpfiiin  43408  pellexlem4  43539  pellqrex  43586  acongtr  43685  acongrep  43687  jm2.23  43703  omlimcl2  43949  onsucf1lem  43976  oege1  44013  nnoeomeqom  44019  cantnfresb  44031  onmcl  44038  tfsconcat0i  44052  ofoafg  44061  ofoafo  44063  ofoaass  44067  ofoacom  44068  naddcnfass  44076  rp-fakeanorass  44219  rp-isfinite6  44224  harval3  44244  inintabss  44284  rfovcnvf1od  44710  clsk1indlem3  44749  ntrclsk13  44777  pm10.55  45059  refsum2cnlem1  45737  axccd2  45925  mptssid  45936  fmuldfeq  46279  climsuse  46304  limclner  46345  climxlim2lem  46539  icccncfext  46581  stoweidlem26  46720  stoweidlem52  46746  stoweidlem57  46751  fourierdlem20  46821  fourierdlem41  46842  fourierdlem52  46852  fourierdlem64  46864  fourierdlem102  46902  fourierdlem114  46914  ovolval4lem1  47343  preimagelt  47393  preimalegt  47394  squeezedltsq  47584  funressneu  47761  afvelrn  47882  elfz2z  48029  2ffzoeq  48042  zplusmodne  48063  addmodne  48064  minusmod5ne  48069  modn0mul  48077  m1modmmod  48078  nndivides2  48098  imasetpreimafvbijlemfv  48128  imasetpreimafvbijlemf1  48130  fargshiftfva  48169  ichreuopeq  48199  2exopprim  48251  reuopreuprim  48252  fmtnoprmfac1  48294  proththd  48343  opoeALTV  48425  evensumeven  48449  sbgoldbalt  48523  evengpop3  48540  evengpoap3  48541  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  wtgoldbnnsum4prm  48544  bgoldbnnsum3prm  48546  tgoldbach  48559  dfclnbgr6  48598  dfsclnbgr6  48600  uhgrimedg  48633  uhgrimprop  48634  isuspgrimlem  48637  isuspgrim  48638  gricushgr  48659  uhgrimisgrgric  48673  isubgr3stgrlem7  48714  uspgrlimlem2  48731  gpgedgel  48792  gpgprismgriedgdmss  48794  gpgedgvtx0  48803  gpgedgiov  48807  gpgedg2ov  48808  gpgedg2iv  48809  gpg5nbgrvtx03starlem2  48811  gpg5nbgrvtx13starlem1  48813  gpg5nbgrvtx13starlem3  48815  gpg5nbgrvtx03star  48822  gpg5nbgr3star  48823  gpg5gricstgr3  48832  pgnbgreunbgrlem4  48861  assintop  48951  uzlidlring  48977  2zrngnmrid  48998  cznrng  49003  lmodvsmdi  49136  lincsum  49186  lincsumcl  49188  el0ldep  49223  ldepspr  49230  lindssnlvec  49243  nn0digval  49357  1arympt1fv  49396  eenglngeehlnmlem1  49494  rrx2linest  49499  line2  49509  itsclc0yqe  49518  r19.41dv  49557  setrec1lem3  50444  aacllem  50578