Theorem anim1i 616

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 22	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	anim12i 614	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:  sylanl1  681  sylanr1  683  eu6im  2575  r19.28v  3168  rmob  3828  eqeuel  4305  preq12nebg  4806  fores  6762  fdmeu  6896  ssimaex  6925  dffv2  6935  exfo  7057  fpropnf1  7222  f1ocoima  7258  oprabv  7427  ndmovass  7555  fun11uni  7884  resf1ext2b  7886  fabexgOLD  7890  f1oabexgOLD  7894  f1iun  7897  soxp  8079  tz7.48lem  8380  tz7.49c  8385  omass  8515  oewordri  8528  omabs  8587  sbthlem9  9033  pssnn  9103  fineqvlem  9176  domunfican  9232  fiint  9237  fsuppsssupp  9294  sup0  9380  inf1  9543  infeq5  9558  cantnfle  9592  rankuni  9787  djuunxp  9845  acndom  9973  acnnum  9974  cdainflem  10110  cfcof  10196  ac6num  10401  ac6s2  10408  brdom5  10451  brdom4  10452  genpnnp  10928  divmulasscom  11833  lediv2a  12050  supmul1  12125  infregelb  12140  nn2ge  12204  btwnz  12632  eluz2b2  12871  uz2mulcl  12876  eqreznegel  12884  xrsupexmnf  13257  xrinfmexpnf  13258  xrsupsslem  13259  xrinfmsslem  13260  supxrun  13268  ioo0  13323  elioo4g  13359  fz0fzelfz0  13588  fz0fzdiffz0  13591  2ffzeq  13603  elfzodifsumelfzo  13686  elfzom1elp1fzo  13687  zpnn0elfzo  13693  elfzom1elp1fzo1  13722  fzonfzoufzol  13726  quoremnn0  13815  zmodidfzoimp  13860  modabs  13863  modaddb  13868  modifeq2int  13895  modaddmulmod  13900  expcl2lem  14035  hashgt23el  14386  hashreshashfun  14401  iswrdsymb  14493  ccatcl  14536  ccatsymb  14545  swrdfv2  14624  swrdsbslen  14627  swrdspsleq  14628  pfxswrd  14668  pfxccatin12lem3  14694  pfxccatpfx2  14699  swrdccat3blem  14701  reuccatpfxs1  14709  repswccat  14748  cshweqdifid  14782  lswco  14801  repsco  14802  s4f1o  14880  trclun  14976  mulre  15083  rediv  15093  imdiv  15100  resqrex  15212  caurcvg2  15640  fsumdifsnconst  15754  modfsummods  15756  tanval  16095  p1modz1  16228  negdvdsb  16241  muldvds1  16249  muldvds2  16250  dvdscmulr  16253  dvdsmulcr  16254  sumodd  16357  divalglem8  16369  divgcdnn  16484  lcmfunsnlem2lem2  16608  lcmfun  16614  2mulprm  16662  maxprmfct  16679  vfermltlALT  16773  modprm0  16776  pcpremul  16814  pcmul  16822  oddprmdvds  16874  prmdvdsprmo  17013  cshwsidrepsw  17064  gsumccat  18809  grpissubg  19122  ecqusaddd  19167  ecqusaddcl  19168  eqg0subg  19171  gim0to0  19244  gsmsymgreqlem2  19406  symgfixfo  19414  fsfnn0gsumfsffz  19958  rnglz  20146  isringrng  20268  irredn0  20403  c0snmgmhm  20442  rimisrngim  20475  zrrnghm  20513  rnghmsubcsetclem2  20609  rhmsubcsetclem2  20638  rhmsubcrngclem2  20644  lsppratlem1  21145  qusmulrng  21280  quscrng  21281  rngqiprngghmlem3  21287  rngqiprnglinlem3  21291  rngqiprngimf1lem  21292  rngqiprnglin  21300  cnfldfunALT  21367  dvdsrzring  21441  mpofrlmd  21757  matinvgcell  22400  mat1dimcrng  22442  dmatscmcl  22468  scmatscm  22478  scmatghm  22498  scmatmhm  22499  ma1repvcl  22535  slesolinv  22645  slesolinvbi  22646  cramerimplem1  22648  cramerimp  22651  cramerlem1  22652  cramer  22656  cpmatacl  22681  cpmatmcl  22684  mat2pmatghm  22695  mat2pmatmul  22696  m2pmfzgsumcl  22713  decpmatmul  22737  decpmatmulsumfsupp  22738  pmatcollpwfi  22747  pm2mpf1  22764  pm2mpghm  22781  pm2mpmhmlem1  22783  monmat2matmon  22789  chpdmatlem2  22804  chpdmat  22806  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  clscld  23012  neiptopnei  23097  2ndcdisj2  23422  comppfsc  23497  tx1stc  23615  opnfbas  23807  fbasfip  23833  alexsublem  24009  alexsubALTlem4  24015  cnextcn  24032  ngpocelbl  24669  cphipval  25210  bcthlem5  25295  vitalilem4  25578  vitalilem5  25579  itg2mulc  25714  bddiblnc  25809  dvcobr  25913  dvcnvlem  25943  dvferm1  25952  dvne0  25978  mdegmullem  26043  plyeq0lem  26175  plyexmo  26279  aalioulem5  26302  aalioulem6  26303  aaliou  26304  cxple2a  26663  cxpaddlelem  26715  cxpaddle  26716  relogbcxpb  26751  bcmono  27240  lgsprme0  27302  gausslemma2dlem0e  27323  gausslemma2dlem1a  27328  gausslemma2dlem6  27335  lgsquadlem2  27344  2lgsoddprm  27379  elno2  27618  cofcutr  27916  colinearalg  28979  axcontlem3  29035  umgrislfupgrlem  29191  edgupgr  29203  usgruspgrb  29252  usgrislfuspgr  29256  edgssv2  29267  umgr2edg  29278  uspgredg2v  29293  usgrexmplef  29328  subupgr  29356  subusgr  29358  nbupgrres  29433  nb3gr2nb  29453  nbupgruvtxres  29476  cusgrres  29517  cusgrsizeindslem  29520  cusgrsizeinds  29521  vtxdun  29550  finrusgrfusgr  29634  cusgrrusgr  29650  pthdifv  29798  spthdep  29802  cycliscrct  29867  crctcshwlkn0lem6  29883  crctcshwlkn0lem7  29884  crctcshtrl  29891  crctcsh  29892  umgr2adedgwlkonALT  30015  elwwlks2  30037  elwspths2spth  30038  rusgrnumwwlk  30046  clwlkclwwlklem2a  30068  clwlkclwwlklem3  30071  clwwisshclwws  30085  wwlksubclwwlk  30128  eleclclwwlknlem2  30131  eupth2lem3lem3  30300  eucrct2eupth1  30314  frgr3v  30345  3vfriswmgr  30348  1to3vfriswmgr  30350  3cyclfrgr  30358  vdgn1frgrv2  30366  frgrwopreglem5  30391  frgrwopreglem5ALT  30392  frrusgrord0lem  30409  frrusgrord0  30410  2clwwlk2clwwlk  30420  extwwlkfab  30422  numclwwlk1lem2fo  30428  friendshipgt3  30468  ex-natded9.20-2  30488  grpoidinvlem3  30577  grpoidinv  30579  nmobndseqi  30850  nmobndseqiALT  30851  hvaddsub4  31149  ocsh  31354  5oalem2  31726  5oalem5  31729  3oalem2  31734  pjjsi  31771  hoadddir  31875  leopmul  32205  stge1i  32309  hatomistici  32433  mdsymlem2  32475  mdsymlem5  32478  addltmulALT  32517  isoun  32775  fsumiunle  32902  lsmsnorb  33451  crefdf  33992  qqhre  34164  esumiun  34238  sxbrsigalem0  34415  dya2iocnei  34426  sxbrsigalem5  34432  sibfinima  34483  eulerpartlemgs2  34524  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemsup  34649  bnj529  34884  bnj945  34916  bnj1098  34926  bnj1533  34994  bnj605  35049  bnj594  35054  bnj607  35058  bnj966  35086  bnj967  35087  bnj996  35098  bnj999  35100  bnj1006  35102  bnj1118  35126  bnj1172  35143  bnj1279  35160  bnj1296  35163  bnj1498  35203  fnrelpredd  35234  lfuhgr3  35302  loop1cycl  35319  cvmsi  35447  satf0op  35559  satffunlem1lem1  35584  satffunlem2lem1  35586  fv2ndcnv  35960  trisegint  36210  funtransport  36213  btwnconn1lem4  36272  btwnconn2  36284  segcon2  36287  outsideofeu  36313  isfne  36521  lukshef-ax2  36597  limsucncmpi  36627  weiunso  36648  bj-nsnid  37377  bj-restn0b  37403  bj-eldiag2  37491  bj-isrvec2  37614  pibt2  37733  unccur  37924  lindsadd  37934  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem30  37971  poimirlem32  37973  heicant  37976  ismblfin  37982  itg2gt0cn  37996  areacirc  38034  opelopab3  38039  isdivrngo  38271  isdrngo2  38279  fldcrngo  38325  flddmn  38379  refrelredund4  39040  mainer2  39281  cmtbr4N  39701  linepsubN  40198  pmapsub  40214  paddasslem14  40279  pclcmpatN  40347  trlval2  40609  cdleme20  40770  cdleme21j  40782  dvalveclem  41471  dia2dimlem7  41516  dvhlveclem  41554  docaclN  41570  dihjat1  41875  mapdhcl  42173  mapdh6dN  42185  mapdh8  42234  hdmap1l6d  42259  hdmap10  42286  hdmaprnlem17N  42309  hdmaplkr  42359  hdmapip0  42361  hgmapvv  42372  aks6d1c4  42563  cmpfiiin  43129  pellexlem4  43260  pellqrex  43307  acongtr  43406  acongrep  43408  jm2.23  43424  omlimcl2  43670  onsucf1lem  43697  oege1  43734  nnoeomeqom  43740  cantnfresb  43752  onmcl  43759  tfsconcat0i  43773  ofoafg  43782  ofoafo  43784  ofoaass  43788  ofoacom  43789  naddcnfass  43797  rp-fakeanorass  43940  rp-isfinite6  43945  harval3  43965  inintabss  44005  rfovcnvf1od  44431  clsk1indlem3  44470  ntrclsk13  44498  pm10.55  44796  refsum2cnlem1  45468  axccd2  45659  mptssid  45670  fmuldfeq  46013  climsuse  46038  limclner  46079  climxlim2lem  46273  icccncfext  46315  stoweidlem26  46454  stoweidlem52  46480  stoweidlem57  46485  fourierdlem20  46555  fourierdlem41  46576  fourierdlem52  46586  fourierdlem64  46598  fourierdlem102  46636  fourierdlem114  46648  ovolval4lem1  47077  preimagelt  47127  preimalegt  47128  squeezedltsq  47318  funressneu  47495  afvelrn  47616  elfz2z  47763  2ffzoeq  47776  zplusmodne  47797  addmodne  47798  minusmod5ne  47803  modn0mul  47811  m1modmmod  47812  nndivides2  47832  imasetpreimafvbijlemfv  47862  imasetpreimafvbijlemf1  47864  fargshiftfva  47903  ichreuopeq  47933  2exopprim  47985  reuopreuprim  47986  fmtnoprmfac1  48028  proththd  48077  opoeALTV  48159  evensumeven  48183  sbgoldbalt  48257  evengpop3  48274  evengpoap3  48275  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  tgoldbach  48293  dfclnbgr6  48332  dfsclnbgr6  48334  uhgrimedg  48367  uhgrimprop  48368  isuspgrimlem  48371  isuspgrim  48372  gricushgr  48393  uhgrimisgrgric  48407  isubgr3stgrlem7  48448  uspgrlimlem2  48465  gpgedgel  48526  gpgprismgriedgdmss  48528  gpgedgvtx0  48537  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem3  48549  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  gpg5gricstgr3  48566  pgnbgreunbgrlem4  48595  assintop  48685  uzlidlring  48711  2zrngnmrid  48732  cznrng  48737  lmodvsmdi  48855  lincsum  48905  lincsumcl  48907  el0ldep  48942  ldepspr  48949  lindssnlvec  48962  nn0digval  49076  1arympt1fv  49115  eenglngeehlnmlem1  49213  rrx2linest  49218  line2  49228  itsclc0yqe  49237  r19.41dv  49277  setrec1lem3  50164  aacllem  50276