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  2605  r19.28v  3196  rmob  3846  eqeuel  4321  preq12nebg  4824  fores  6792  fdmeu  6927  ssimaex  6956  dffv2  6966  exfo  7090  fpropnf1  7255  f1ocoima  7291  oprabv  7460  ndmovass  7588  fun11uni  7918  resf1ext2b  7920  f1iun  7929  soxp  8113  tz7.48lem  8416  tz7.49c  8421  omass  8553  oewordri  8566  omabs  8625  sbthlem9  9071  pssnn  9141  fineqvlem  9214  domunfican  9269  fiint  9274  fsuppsssupp  9329  sup0  9415  inf1  9579  infeq5  9594  cantnfle  9628  rankuni  9823  djuunxp  9895  acndom  10023  acnnum  10024  cdainflem  10159  cfcof  10246  ac6num  10451  ac6s2  10458  brdom5  10501  brdom4  10502  genpnnp  10978  divmulasscom  11884  lediv2a  12100  supmul1  12175  infregelb  12190  nn2ge  12254  btwnz  12690  eluz2b2  12936  uz2mulcl  12941  eqreznegel  12949  xrsupexmnf  13322  xrinfmexpnf  13323  xrsupsslem  13324  xrinfmsslem  13325  supxrun  13333  ioo0  13388  elioo4g  13424  fz0fzelfz0  13653  fz0fzdiffz0  13656  2ffzeq  13668  elfzodifsumelfzo  13751  elfzom1elp1fzo  13752  zpnn0elfzo  13758  elfzom1elp1fzo1  13787  fzonfzoufzol  13791  quoremnn0  13880  zmodidfzoimp  13925  modabs  13928  modaddb  13933  modifeq2int  13960  modaddmulmod  13965  expcl2lem  14100  hashgt23el  14451  hashreshashfun  14466  iswrdsymb  14558  ccatcl  14601  ccatsymb  14610  swrdfv2  14689  swrdsbslen  14692  swrdspsleq  14693  pfxswrd  14733  pfxccatin12lem3  14759  pfxccatpfx2  14764  swrdccat3blem  14766  reuccatpfxs1  14774  repswccat  14813  cshweqdifid  14847  lswco  14866  repsco  14867  s4f1o  14945  trclun  15041  mulre  15162  rediv  15172  imdiv  15179  resqrex  15291  caurcvg2  15719  fsumdifsnconst  15833  modfsummods  15835  tanval  16174  p1modz1  16307  negdvdsb  16320  muldvds1  16328  muldvds2  16329  dvdscmulr  16332  dvdsmulcr  16333  sumodd  16436  divalglem8  16448  divgcdnn  16563  lcmfunsnlem2lem2  16687  lcmfun  16693  2mulprm  16741  maxprmfct  16758  vfermltlALT  16852  modprm0  16855  pcpremul  16893  pcmul  16901  oddprmdvds  16953  prmdvdsprmo  17092  cshwsidrepsw  17143  gsumccat  18890  grpissubg  19204  ecqusaddd  19254  ecqusaddcl  19255  eqg0subg  19258  gim0to0  19330  gsmsymgreqlem2  19492  symgfixfo  19500  fsfnn0gsumfsffz  20044  rnglz  20234  isringrng  20361  irredn0  20496  c0snmgmhm  20535  rimisrngim  20571  zrrnghm  20612  rnghmsubcsetclem2  20708  rhmsubcsetclem2  20737  rhmsubcrngclem2  20743  lsppratlem1  21240  qusmulrng  21384  quscrng  21385  rngqiprngghmlem3  21391  rngqiprnglinlem3  21395  rngqiprngimf1lem  21396  rngqiprnglin  21404  cnfldfunALT  21497  dvdsrzring  21571  mpofrlmd  21887  matinvgcell  22553  mat1dimcrng  22595  dmatscmcl  22621  scmatscm  22631  scmatghm  22651  scmatmhm  22652  ma1repvcl  22688  slesolinv  22798  slesolinvbi  22799  cramerimplem1  22801  cramerimp  22804  cramerlem1  22805  cramer  22809  cpmatacl  22834  cpmatmcl  22837  mat2pmatghm  22848  mat2pmatmul  22849  m2pmfzgsumcl  22866  decpmatmul  22890  decpmatmulsumfsupp  22891  pmatcollpwfi  22900  pm2mpf1  22917  pm2mpghm  22934  pm2mpmhmlem1  22936  monmat2matmon  22942  chpdmatlem2  22957  chpdmat  22959  cpmadugsumlemB  22992  cpmadugsumlemC  22993  cpmadugsumlemF  22994  clscld  23165  neiptopnei  23250  2ndcdisj2  23575  comppfsc  23650  tx1stc  23768  opnfbas  23960  fbasfip  23986  alexsublem  24162  alexsubALTlem4  24168  cnextcn  24185  ngpocelbl  24822  cphipval  25363  bcthlem5  25448  vitalilem4  25731  vitalilem5  25732  itg2mulc  25867  bddiblnc  25962  dvcobr  26066  dvcnvlem  26096  dvferm1  26105  dvne0  26131  mdegmullem  26196  plyeq0lem  26328  plyexmo  26435  aalioulem5  26458  aalioulem6  26459  aaliou  26460  cxple2a  26822  cxpaddlelem  26874  cxpaddle  26875  relogbcxpb  26910  bcmono  27399  lgsprme0  27461  gausslemma2dlem0e  27482  gausslemma2dlem1a  27487  gausslemma2dlem6  27494  lgsquadlem2  27503  2lgsoddprm  27538  elno2  27776  cofcutr  28075  colinearalg  29169  axcontlem3  29225  umgrislfupgrlem  29381  edgupgr  29393  usgruspgrb  29442  usgrislfuspgr  29446  edgssv2  29457  umgr2edg  29468  uspgredg2v  29483  usgrexmplef  29518  subupgr  29546  subusgr  29548  nbupgrres  29623  nb3gr2nb  29643  nbupgruvtxres  29666  cusgrres  29707  cusgrsizeindslem  29710  cusgrsizeinds  29711  vtxdun  29740  finrusgrfusgr  29824  cusgrrusgr  29840  pthdifv  29988  spthdep  29992  cycliscrct  30057  crctcshwlkn0lem6  30073  crctcshwlkn0lem7  30074  crctcshtrl  30081  crctcsh  30082  umgr2adedgwlkonALT  30205  elwwlks2  30227  elwspths2spth  30228  rusgrnumwwlk  30236  clwlkclwwlklem2a  30258  clwlkclwwlklem3  30261  clwwisshclwws  30275  wwlksubclwwlk  30318  eleclclwwlknlem2  30321  eupth2lem3lem3  30490  eucrct2eupth1  30504  frgr3v  30535  3vfriswmgr  30538  1to3vfriswmgr  30540  3cyclfrgr  30548  vdgn1frgrv2  30556  frgrwopreglem5  30581  frgrwopreglem5ALT  30582  frrusgrord0lem  30599  frrusgrord0  30600  2clwwlk2clwwlk  30610  extwwlkfab  30612  numclwwlk1lem2fo  30618  friendshipgt3  30658  ex-natded9.20-2  30678  grpoidinvlem3  30767  grpoidinv  30769  nmobndseqi  31040  nmobndseqiALT  31041  hvaddsub4  31339  ocsh  31544  5oalem2  31916  5oalem5  31919  3oalem2  31924  pjjsi  31961  hoadddir  32065  leopmul  32395  stge1i  32499  hatomistici  32623  mdsymlem2  32665  mdsymlem5  32668  addltmulALT  32707  isoun  32959  fsumiunle  33086  lsmsnorb  33620  crefdf  34155  qqhre  34327  esumiun  34401  sxbrsigalem0  34578  dya2iocnei  34589  sxbrsigalem5  34595  sibfinima  34646  eulerpartlemgs2  34687  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemsup  34812  bnj529  35047  bnj945  35079  bnj1098  35089  bnj1533  35157  bnj605  35212  bnj594  35217  bnj607  35221  bnj966  35249  bnj967  35250  bnj996  35261  bnj999  35263  bnj1006  35265  bnj1118  35289  bnj1172  35306  bnj1279  35323  bnj1296  35326  bnj1498  35366  fnrelpredd  35397  lfuhgr3  35483  loop1cycl  35500  cvmsi  35628  satf0op  35740  satffunlem1lem1  35765  satffunlem2lem1  35767  fv2ndcnv  36141  trisegint  36391  funtransport  36394  btwnconn1lem4  36453  btwnconn2  36465  segcon2  36468  outsideofeu  36494  isfne  36712  lukshef-ax2  36788  limsucncmpi  36818  weiunso  36839  bj-nsnid  37567  bj-restn0b  37593  bj-eldiag2  37681  bj-isrvec2  37804  pibt2  37923  unccur  38114  lindsadd  38124  lindsenlbs  38126  matunitlindflem1  38127  matunitlindflem2  38128  poimirlem26  38157  poimirlem27  38158  poimirlem29  38160  poimirlem30  38161  poimirlem32  38163  heicant  38166  ismblfin  38172  itg2gt0cn  38186  areacirc  38224  opelopab3  38229  isdivrngo  38461  isdrngo2  38469  fldcrngo  38515  flddmn  38569  refrelredund4  39230  mainer2  39471  cmtbr4N  39891  linepsubN  40388  pmapsub  40404  paddasslem14  40469  pclcmpatN  40537  trlval2  40799  cdleme20  40960  cdleme21j  40972  dvalveclem  41661  dia2dimlem7  41706  dvhlveclem  41744  docaclN  41760  dihjat1  42065  mapdhcl  42363  mapdh6dN  42375  mapdh8  42424  hdmap1l6d  42449  hdmap10  42476  hdmaprnlem17N  42499  hdmaplkr  42549  hdmapip0  42551  hgmapvv  42562  aks6d1c4  42753  cmpfiiin  43290  pellexlem4  43421  pellqrex  43468  acongtr  43567  acongrep  43569  jm2.23  43585  omlimcl2  43831  onsucf1lem  43858  oege1  43895  nnoeomeqom  43901  cantnfresb  43913  onmcl  43920  tfsconcat0i  43934  ofoafg  43943  ofoafo  43945  ofoaass  43949  ofoacom  43950  naddcnfass  43958  rp-fakeanorass  44101  rp-isfinite6  44106  harval3  44126  inintabss  44166  rfovcnvf1od  44592  clsk1indlem3  44631  ntrclsk13  44659  pm10.55  44943  refsum2cnlem1  45615  axccd2  45803  mptssid  45814  fmuldfeq  46157  climsuse  46182  limclner  46223  climxlim2lem  46417  icccncfext  46459  stoweidlem26  46598  stoweidlem52  46624  stoweidlem57  46629  fourierdlem20  46699  fourierdlem41  46720  fourierdlem52  46730  fourierdlem64  46742  fourierdlem102  46780  fourierdlem114  46792  ovolval4lem1  47221  preimagelt  47271  preimalegt  47272  squeezedltsq  47462  funressneu  47639  afvelrn  47760  elfz2z  47907  2ffzoeq  47920  zplusmodne  47941  addmodne  47942  minusmod5ne  47947  modn0mul  47955  m1modmmod  47956  nndivides2  47976  imasetpreimafvbijlemfv  48006  imasetpreimafvbijlemf1  48008  fargshiftfva  48047  ichreuopeq  48077  2exopprim  48129  reuopreuprim  48130  fmtnoprmfac1  48172  proththd  48221  opoeALTV  48303  evensumeven  48327  sbgoldbalt  48401  evengpop3  48418  evengpoap3  48419  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  wtgoldbnnsum4prm  48422  bgoldbnnsum3prm  48424  tgoldbach  48437  dfclnbgr6  48476  dfsclnbgr6  48478  uhgrimedg  48511  uhgrimprop  48512  isuspgrimlem  48515  isuspgrim  48516  gricushgr  48537  uhgrimisgrgric  48551  isubgr3stgrlem7  48592  uspgrlimlem2  48609  gpgedgel  48670  gpgprismgriedgdmss  48672  gpgedgvtx0  48681  gpgedgiov  48685  gpgedg2ov  48686  gpgedg2iv  48687  gpg5nbgrvtx03starlem2  48689  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem3  48693  gpg5nbgrvtx03star  48700  gpg5nbgr3star  48701  gpg5gricstgr3  48710  pgnbgreunbgrlem4  48739  assintop  48829  uzlidlring  48855  2zrngnmrid  48876  cznrng  48881  lmodvsmdi  49010  lincsum  49060  lincsumcl  49062  el0ldep  49097  ldepspr  49104  lindssnlvec  49117  nn0digval  49231  1arympt1fv  49270  eenglngeehlnmlem1  49368  rrx2linest  49373  line2  49383  itsclc0yqe  49392  r19.41dv  49431  setrec1lem3  50318  aacllem  50430