Theorem anim1i 614

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 612	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 206  df-an 396

This theorem is referenced by:  sylanl1  676  sylanr1  678  eu6im  2575  r19.28v  3110  rmob  3819  eqeuel  4293  preq12nebg  4790  fores  6682  ssimaex  6835  dffv2  6845  exfo  6963  fpropnf1  7121  oprabv  7313  ndmovass  7438  fun11uni  7753  fabexg  7755  f1oabexg  7757  f1iun  7760  soxp  7941  tz7.48lem  8242  tz7.49c  8247  omass  8373  oewordri  8385  omabs  8441  sbthlem9  8831  pssnn  8913  fineqvlem  8966  pssnnOLD  8969  domunfican  9017  fiint  9021  fsuppsssupp  9074  sup0  9155  inf1  9310  infeq5  9325  cantnfle  9359  rankuni  9552  djuunxp  9610  acndom  9738  acnnum  9739  cdainflem  9874  cfcof  9961  ac6num  10166  ac6s2  10173  brdom5  10216  brdom4  10217  genpnnp  10692  divmulasscom  11587  lediv2a  11799  supmul1  11874  infregelb  11889  nn2ge  11930  btwnz  12352  eluz2b2  12590  uz2mulcl  12595  eqreznegel  12603  xrsupexmnf  12968  xrinfmexpnf  12969  xrsupsslem  12970  xrinfmsslem  12971  supxrun  12979  ioo0  13033  elioo4g  13068  fz0fzelfz0  13291  fz0fzdiffz0  13294  2ffzeq  13306  elfzodifsumelfzo  13381  elfzom1elp1fzo  13382  zpnn0elfzo  13388  elfzom1elp1fzo1  13415  fzonfzoufzol  13418  quoremnn0  13504  zmodidfzoimp  13549  modabs  13552  modmuladd  13561  modifeq2int  13581  modaddmulmod  13586  expcl2lem  13722  hashgt23el  14067  hashreshashfun  14082  iswrdsymb  14162  ccatcl  14205  ccatsymb  14215  swrdfv2  14302  swrdsbslen  14305  swrdspsleq  14306  pfxswrd  14347  pfxccatin12lem3  14373  pfxccatpfx2  14378  swrdccat3blem  14380  reuccatpfxs1  14388  repswccat  14427  cshweqdifid  14461  lswco  14480  repsco  14481  s4f1o  14559  ccat2s1fvwALTOLD  14598  trclun  14653  mulre  14760  rediv  14770  imdiv  14777  resqrex  14890  caurcvg2  15317  fsumdifsnconst  15431  modfsummods  15433  tanval  15765  p1modz1  15898  negdvdsb  15910  muldvds1  15918  muldvds2  15919  dvdscmulr  15922  dvdsmulcr  15923  sumodd  16025  divalglem8  16037  divgcdnn  16150  lcmfunsnlem2lem2  16272  lcmfun  16278  2mulprm  16326  maxprmfct  16342  vfermltlALT  16431  modprm0  16434  pcpremul  16472  pcmul  16480  oddprmdvds  16532  prmdvdsprmo  16671  cshwsidrepsw  16723  gsumccat  18395  grpissubg  18690  gsmsymgreqlem2  18954  symgfixfo  18962  fsfnn0gsumfsffz  19499  irredn0  19860  gim0to0  19901  lsppratlem1  20324  dvdsrzring  20595  mpofrlmd  20894  matinvgcell  21492  mat1dimcrng  21534  dmatscmcl  21560  scmatscm  21570  scmatghm  21590  scmatmhm  21591  ma1repvcl  21627  slesolinv  21737  slesolinvbi  21738  cramerimplem1  21740  cramerimp  21743  cramerlem1  21744  cramer  21748  cpmatacl  21773  cpmatmcl  21776  mat2pmatghm  21787  mat2pmatmul  21788  m2pmfzgsumcl  21805  decpmatmul  21829  decpmatmulsumfsupp  21830  pmatcollpwfi  21839  pm2mpf1  21856  pm2mpghm  21873  pm2mpmhmlem1  21875  monmat2matmon  21881  chpdmatlem2  21896  chpdmat  21898  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  clscld  22106  neiptopnei  22191  2ndcdisj2  22516  comppfsc  22591  tx1stc  22709  opnfbas  22901  fbasfip  22927  alexsublem  23103  alexsubALTlem4  23109  cnextcn  23126  ngpocelbl  23774  cphipval  24312  bcthlem5  24397  vitalilem4  24680  vitalilem5  24681  itg2mulc  24817  bddiblnc  24911  dvcobr  25015  dvcnvlem  25045  dvferm1  25054  dvne0  25080  mdegmullem  25148  plyeq0lem  25276  plyexmo  25378  aalioulem5  25401  aalioulem6  25402  aaliou  25403  cxple2a  25759  cxpaddlelem  25809  cxpaddle  25810  relogbcxpb  25842  bcmono  26330  lgsprme0  26392  gausslemma2dlem0e  26413  gausslemma2dlem1a  26418  gausslemma2dlem6  26425  lgsquadlem2  26434  2lgsoddprm  26469  colinearalg  27181  axcontlem3  27237  umgrislfupgrlem  27395  edgupgr  27407  usgruspgrb  27454  usgrislfuspgr  27457  edgssv2  27468  umgr2edg  27479  uspgredg2v  27494  usgrexmplef  27529  subupgr  27557  subusgr  27559  nbupgrres  27634  nb3gr2nb  27654  nbupgruvtxres  27677  cusgrres  27718  cusgrsizeindslem  27721  cusgrsizeinds  27722  vtxdun  27751  finrusgrfusgr  27835  cusgrrusgr  27851  spthdep  28003  cycliscrct  28068  crctcshwlkn0lem6  28081  crctcshwlkn0lem7  28082  crctcshtrl  28089  crctcsh  28090  umgr2adedgwlkonALT  28213  elwwlks2  28232  elwspths2spth  28233  rusgrnumwwlk  28241  clwlkclwwlklem2a  28263  clwlkclwwlklem3  28266  clwwisshclwws  28280  wwlksubclwwlk  28323  eleclclwwlknlem2  28326  eupth2lem3lem3  28495  eucrct2eupth1  28509  frgr3v  28540  3vfriswmgr  28543  1to3vfriswmgr  28545  3cyclfrgr  28553  vdgn1frgrv2  28561  frgrwopreglem5  28586  frgrwopreglem5ALT  28587  frrusgrord0lem  28604  frrusgrord0  28605  2clwwlk2clwwlk  28615  extwwlkfab  28617  numclwwlk1lem2fo  28623  friendshipgt3  28663  ex-natded9.20-2  28683  grpoidinvlem3  28769  grpoidinv  28771  nmobndseqi  29042  nmobndseqiALT  29043  hvaddsub4  29341  ocsh  29546  5oalem2  29918  5oalem5  29921  3oalem2  29926  pjjsi  29963  hoadddir  30067  leopmul  30397  stge1i  30501  hatomistici  30625  mdsymlem2  30667  mdsymlem5  30670  addltmulALT  30709  isoun  30936  fsumiunle  31045  lsmsnorb  31481  crefdf  31700  qqhre  31870  esumiun  31962  sxbrsigalem0  32138  dya2iocnei  32149  sxbrsigalem5  32155  sibfinima  32206  eulerpartlemgs2  32247  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemsup  32371  bnj529  32621  bnj945  32653  bnj1098  32663  bnj1533  32732  bnj605  32787  bnj594  32792  bnj607  32796  bnj966  32824  bnj967  32825  bnj996  32836  bnj999  32838  bnj1006  32840  bnj1118  32864  bnj1172  32881  bnj1279  32898  bnj1296  32901  bnj1498  32941  fnrelpredd  32961  lfuhgr3  32981  loop1cycl  32999  cvmsi  33127  satf0op  33239  satffunlem1lem1  33264  satffunlem2lem1  33266  fv2ndcnv  33658  elno2  33784  cofcutr  34019  trisegint  34257  funtransport  34260  btwnconn1lem4  34319  btwnconn2  34331  segcon2  34334  outsideofeu  34360  isfne  34455  lukshef-ax2  34531  limsucncmpi  34561  bj-nsnid  35168  bj-restn0b  35189  bj-eldiag2  35275  bj-isrvec2  35398  pibt2  35515  unccur  35687  lindsadd  35697  lindsenlbs  35699  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem30  35734  poimirlem32  35736  heicant  35739  ismblfin  35745  itg2gt0cn  35759  areacirc  35797  opelopab3  35802  isdivrngo  36035  isdrngo2  36043  fldcrng  36089  flddmn  36143  refrelredund4  36675  cmtbr4N  37196  linepsubN  37693  pmapsub  37709  paddasslem14  37774  pclcmpatN  37842  trlval2  38104  cdleme20  38265  cdleme21j  38277  dvalveclem  38966  dia2dimlem7  39011  dvhlveclem  39049  docaclN  39065  dihjat1  39370  mapdhcl  39668  mapdh6dN  39680  mapdh8  39729  hdmap1l6d  39754  hdmap10  39781  hdmaprnlem17N  39804  hdmaplkr  39854  hdmapip0  39856  hgmapvv  39867  cmpfiiin  40435  pellexlem4  40570  pellqrex  40617  acongtr  40716  acongrep  40718  jm2.23  40734  rp-fakeanorass  41018  rp-isfinite6  41023  harval3  41041  inintabss  41075  rfovcnvf1od  41501  clsk1indlem3  41542  ntrclsk13  41570  pm10.55  41876  refsum2cnlem1  42469  axccd2  42658  mptssid  42674  fmuldfeq  43014  climsuse  43039  limclner  43082  climxlim2lem  43276  icccncfext  43318  stoweidlem26  43457  stoweidlem52  43483  stoweidlem57  43488  fourierdlem20  43558  fourierdlem41  43579  fourierdlem52  43589  fourierdlem64  43601  fourierdlem102  43639  fourierdlem114  43651  ovolval4lem1  44077  preimagelt  44126  preimalegt  44127  funressneu  44428  afvelrn  44547  elfz2z  44695  2ffzoeq  44708  imasetpreimafvbijlemfv  44742  imasetpreimafvbijlemf1  44744  fargshiftfva  44783  ichreuopeq  44813  2exopprim  44865  reuopreuprim  44866  fmtnoprmfac1  44905  proththd  44954  opoeALTV  45023  evensumeven  45047  sbgoldbalt  45121  evengpop3  45138  evengpoap3  45139  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  tgoldbach  45157  isomushgr  45166  assintop  45291  isringrng  45327  rnglz  45330  c0snmgmhm  45360  zrrnghm  45363  uzlidlring  45375  2zrngnmrid  45396  cznrng  45401  rnghmsubcsetclem2  45422  rhmsubcsetclem2  45468  rhmsubcrngclem2  45474  lmodvsmdi  45606  lincsum  45658  lincsumcl  45660  el0ldep  45695  ldepspr  45702  lindssnlvec  45715  modn0mul  45754  m1modmmod  45755  nn0digval  45834  1arympt1fv  45873  eenglngeehlnmlem1  45971  rrx2linest  45976  line2  45986  itsclc0yqe  45995  r19.41dv  46035  setrec1lem3  46281  aacllem  46391