Theorem anim1i 627

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylanl1  693  sylanr1  695  ax12ev2c  2217  eu6im  2601  r19.28v  3194  rmob  3837  eqeuel  4313  preq12nebg  4823  fores  6798  fdmeu  6933  ssimaex  6962  dffv2  6972  exfo  7097  fpropnf1  7263  f1ocoima  7303  oprabv  7472  ndmovass  7601  fun11uni  7934  resf1ext2b  7936  f1iun  7945  soxp  8130  tz7.48lemOLD  8435  tz7.49c  8440  omass  8572  oewordri  8585  omabs  8644  sbthlem9  9098  pssnn  9168  fineqvlem  9241  domunfican  9297  fiint  9302  fsuppsssupp  9357  sup0  9443  inf1  9607  infeq5  9622  cantnfle  9656  rankuni  9860  setrec1lem3  9950  djuunxp  9983  acndom  10111  acnnum  10112  cdainflem  10247  cfcof  10333  ac6num  10538  ac6s2  10545  brdom5  10589  brdom4  10590  genpnnp  11071  divmulasscom  11979  lediv2a  12192  supmul1  12267  infregelb  12282  nn2ge  12346  btwnz  12783  eluz2b2  13029  uz2mulcl  13034  eqreznegel  13042  xrsupexmnf  13416  xrinfmexpnf  13417  xrsupsslem  13418  xrinfmsslem  13419  supxrun  13427  ioo0  13482  elioo4g  13518  fz0fzelfz0  13748  fz0fzdiffz0  13751  2ffzeq  13763  elfzodifsumelfzo  13846  elfzom1elp1fzo  13847  zpnn0elfzo  13853  elfzom1elp1fzo1  13882  fzonfzoufzol  13886  quoremnn0  13976  zmodidfzoimp  14021  modabs  14024  modaddb  14029  modifeq2int  14056  modaddmulmod  14061  expcl2lem  14196  hashgt23el  14549  hashreshashfun  14564  iswrdsymb  14656  ccatcl  14699  ccatsymb  14708  swrdfv2  14791  swrdsbslen  14794  swrdspsleq  14795  pfxswrd  14835  pfxccatin12lem3  14861  pfxccatpfx2  14866  swrdccat3blem  14868  reuccatpfxs1  14876  repswccat  14917  cshweqdifid  14951  lswco  14970  repsco  14971  s4f1o  15049  trclun  15147  mulre  15268  rediv  15278  imdiv  15285  resqrex  15397  caurcvg2  15825  fsumdifsnconst  15938  modfsummods  15940  tanval  16276  p1modz1  16409  negdvdsb  16422  muldvds1  16430  muldvds2  16431  dvdscmulr  16434  dvdsmulcr  16435  sumodd  16538  divalglem8  16550  divgcdnn  16667  lcmfunsnlem2lem2  16794  lcmfun  16800  2mulprm  16848  maxprmfct  16865  vfermltlALT  16960  modprm0  16963  pcpremul  17001  pcmul  17009  oddprmdvds  17061  prmdvdsprmo  17200  cshwsidrepsw  17251  gsumccat  19017  grpissubg  19337  ecqusaddd  19387  ecqusaddcl  19388  eqg0subg  19391  gim0to0  19463  gsmsymgreqlem2  19625  symgfixfo  19633  fsfnn0gsumfsffz  20177  rnglz  20367  isringrng  20496  irredn0  20633  c0snmgmhm  20672  rimisrngim  20715  zrrnghm  20768  rnghmsubcsetclem2  20864  rhmsubcsetclem2  20893  rhmsubcrngclem2  20899  lsppratlem1  21405  qusmulrng  21558  quscrng  21559  rngqiprngghmlem3  21565  rngqiprnglinlem3  21569  rngqiprngimf1lem  21570  rngqiprnglin  21578  cnfldfunALT  21673  dvdsrzring  21747  mpofrlmd  22063  lindsenlbs  22137  matinvgcell  22730  mat1dimcrng  22772  dmatscmcl  22798  scmatscm  22808  scmatghm  22828  scmatmhm  22829  ma1repvcl  22865  matunitlindflem1  22974  matunitlindflem2  22975  slesolinv  22978  slesolinvbi  22979  cramerimplem1  22981  cramerimp  22984  cramerlem1  22985  cramer  22989  cpmatacl  23014  cpmatmcl  23017  mat2pmatghm  23028  mat2pmatmul  23029  m2pmfzgsumcl  23046  decpmatmul  23070  decpmatmulsumfsupp  23071  pmatcollpwfi  23080  pm2mpf1  23097  pm2mpghm  23114  pm2mpmhmlem1  23116  monmat2matmon  23122  chpdmatlem2  23137  chpdmat  23139  cpmadugsumlemB  23172  cpmadugsumlemC  23173  cpmadugsumlemF  23174  clscld  23345  neiptopnei  23430  2ndcdisj2  23756  comppfsc  23831  tx1stc  23949  opnfbas  24141  fbasfip  24167  alexsublem  24343  alexsubALTlem4  24349  cnextcn  24366  ngpocelbl  25003  cphipval  25544  bcthlem5  25629  vitalilem4  25912  vitalilem5  25913  itg2mulc  26048  bddiblnc  26142  dvcobr  26246  dvcnvlem  26276  dvferm1  26285  dvne0  26311  mdegmullem  26376  plyeq0lem  26509  plyexmo  26618  aalioulem5  26645  aalioulem6  26646  aaliou  26647  cxple2a  27009  cxpaddlelem  27061  cxpaddle  27062  relogbcxpb  27097  bcmono  27586  lgsprme0  27648  gausslemma2dlem0e  27669  gausslemma2dlem1a  27674  gausslemma2dlem6  27681  lgsquadlem2  27690  2lgsoddprm  27725  fltoprmlem1  27975  elno2  27993  cofcutr  28292  colinearalg  29470  axcontlem3  29526  umgrislfupgrlem  29682  edgupgr  29694  lfuhgr3  29710  usgruspgrb  29746  usgrislfuspgr  29750  edgssv2  29761  umgr2edg  29772  uspgredg2v  29787  usgrexmplef  29822  subupgr  29850  subusgr  29852  nbupgrres  29927  nb3gr2nb  29947  nbupgruvtxres  29970  cusgrres  30011  cusgrsizeindslem  30014  cusgrsizeinds  30015  vtxdun  30044  finrusgrfusgr  30128  cusgrrusgr  30144  pthdifv  30298  spthdep  30302  cycliscrct  30369  crctcshwlkn0lem6  30386  crctcshwlkn0lem7  30387  crctcshtrl  30394  crctcsh  30395  umgr2adedgwlkonALT  30518  elwwlks2  30540  elwspths2spth  30541  rusgrnumwwlk  30549  clwlkclwwlklem2a  30571  clwlkclwwlklem3  30574  clwwisshclwws  30588  wwlksubclwwlk  30631  eleclclwwlknlem2  30634  loop1cycl  30726  eupth2lem3lem3  30813  eucrct2eupth1  30827  frgr3v  30858  3vfriswmgr  30861  1to3vfriswmgr  30863  3cyclfrgr  30871  vdgn1frgrv2  30879  frgrwopreglem5  30904  frgrwopreglem5ALT  30905  frrusgrord0lem  30922  frrusgrord0  30923  2clwwlk2clwwlk  30933  extwwlkfab  30935  numclwwlk1lem2fo  30941  friendshipgt3  30981  ex-natded9.20-2  31001  grpoidinvlem3  31090  grpoidinv  31092  nmobndseqi  31363  nmobndseqiALT  31364  hvaddsub4  31662  ocsh  31867  5oalem2  32239  5oalem5  32242  3oalem2  32247  pjjsi  32284  hoadddir  32388  leopmul  32718  stge1i  32822  hatomistici  32946  mdsymlem2  32988  mdsymlem5  32991  addltmulALT  33030  isoun  33277  fsumiunle  33402  lsmsnorb  33928  crefdf  34462  qqhre  34634  esumiun  34708  sxbrsigalem0  34886  dya2iocnei  34897  sxbrsigalem5  34903  sibfinima  34954  eulerpartlemgs2  34995  ballotlemfc0  35108  ballotlemfcc  35109  ballotlemsup  35120  bnj529  35355  bnj945  35387  bnj1098  35397  bnj1533  35465  bnj605  35520  bnj594  35525  bnj607  35529  bnj966  35557  bnj967  35558  bnj996  35569  bnj999  35571  bnj1006  35573  bnj1118  35597  bnj1172  35614  bnj1279  35631  bnj1296  35634  bnj1498  35674  fnrelpredd  35699  cvmsi  35999  satf0op  36111  satffunlem1lem1  36136  satffunlem2lem1  36138  fv2ndcnv  36512  trisegint  36763  funtransport  36766  btwnconn1lem4  36825  btwnconn2  36837  segcon2  36840  outsideofeu  36866  isfne  37097  lukshef-ax2  37173  limsucncmpi  37203  weiunso  37224  bj-nsnid  37953  bj-restn0b  37980  bj-eldiag2  38066  bj-isrvec2  38189  pibt2  38308  unccur  38494  lindsadd  38504  poimirlem26  38532  poimirlem27  38533  poimirlem29  38535  poimirlem30  38536  poimirlem32  38538  heicant  38541  ismblfin  38547  itg2gt0cn  38561  areacirc  38599  impprop  38612  opelopab3  38620  isdivrngo  38852  isdrngo2  38860  fldcrngo  38906  flddmn  38960  refrelredund4  39619  mainer2  39860  cmtbr4N  40280  linepsubN  40777  pmapsub  40793  paddasslem14  40858  pclcmpatN  40926  trlval2  41188  cdleme20  41349  cdleme21j  41361  dvalveclem  42050  dia2dimlem7  42095  dvhlveclem  42133  docaclN  42149  dihjat1  42454  mapdhcl  42752  mapdh6dN  42764  mapdh8  42813  hdmap1l6d  42838  hdmap10  42865  hdmaprnlem17N  42888  hdmaplkr  42938  hdmapip0  42940  hgmapvv  42951  aks6d1c4  43142  cmpfiiin  43661  pellexlem4  43792  pellqrex  43839  acongtr  43938  acongrep  43940  jm2.23  43956  omlimcl2  44202  onsucf1lem  44229  oege1  44266  nnoeomeqom  44272  cantnfresb  44284  onmcl  44291  tfsconcat0i  44305  ofoafg  44314  ofoafo  44316  ofoaass  44320  ofoacom  44321  naddcnfass  44329  rp-fakeanorass  44472  rp-isfinite6  44477  harval3  44497  inintabss  44537  rfovcnvf1od  44963  clsk1indlem3  45002  ntrclsk13  45030  pm10.55  45312  refsum2cnlem1  45997  axccd2  46185  mptssid  46196  fmuldfeq  46539  climsuse  46564  limclner  46605  climxlim2lem  46799  icccncfext  46841  stoweidlem26  46980  stoweidlem52  47006  stoweidlem57  47011  fourierdlem20  47081  fourierdlem41  47102  fourierdlem52  47112  fourierdlem64  47124  fourierdlem102  47162  fourierdlem114  47174  ovolval4lem1  47603  preimagelt  47653  preimalegt  47654  squeezedltsq  47856  funressneu  48061  afvelrn  48182  elfz2z  48329  2ffzoeq  48342  zplusmodne  48363  addmodne  48364  minusmod5ne  48369  modn0mul  48377  m1modmmod  48378  nndivides2  48398  imasetpreimafvbijlemfv  48428  imasetpreimafvbijlemf1  48430  fargshiftfva  48469  ichreuopeq  48499  2exopprim  48551  reuopreuprim  48552  fmtnoprmfac1  48594  proththd  48643  opoeALTV  48725  evensumeven  48749  sbgoldbalt  48823  evengpop3  48840  evengpoap3  48841  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  wtgoldbnnsum4prm  48844  bgoldbnnsum3prm  48846  tgoldbach  48859  dfclnbgr6  48898  dfsclnbgr6  48900  uhgrimedg  48933  uhgrimprop  48934  isuspgrimlem  48937  isuspgrim  48938  gricushgr  48959  uhgrimisgrgric  48973  isubgr3stgrlem7  49014  uspgrlimlem2  49031  gpgedgel  49092  gpgprismgriedgdmss  49094  gpgedgvtx0  49103  gpgedgiov  49107  gpgedg2ov  49108  gpgedg2iv  49109  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem3  49115  gpg5nbgrvtx03star  49122  gpg5nbgr3star  49123  gpg5gricstgr3  49132  pgnbgreunbgrlem4  49161  assintop  49250  uzlidlring  49276  2zrngnmrid  49297  cznrng  49302  lmodvsmdi  49435  lincsum  49485  lincsumcl  49487  el0ldep  49522  ldepspr  49529  lindssnlvec  49542  nn0digval  49656  1arympt1fv  49695  eenglngeehlnmlem1  49793  rrx2linest  49798  line2  49808  itsclc0yqe  49817  r19.41dv  49856  aacllem  50883