Theorem anim1i 615

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 613	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  680  sylanr1  682  eu6im  2572  r19.28v  3187  rmob  3898  eqeuel  4370  preq12nebg  4867  fores  6830  fdmeu  6964  ssimaex  6993  dffv2  7003  exfo  7124  fpropnf1  7286  f1ocoima  7322  oprabv  7492  ndmovass  7620  fun11uni  7955  fabexgOLD  7959  f1oabexgOLD  7963  f1iun  7966  soxp  8152  tz7.48lem  8479  tz7.49c  8484  omass  8616  oewordri  8628  omabs  8687  sbthlem9  9129  pssnn  9206  fineqvlem  9295  domunfican  9358  fiint  9363  fiintOLD  9364  fsuppsssupp  9418  sup0  9503  inf1  9659  infeq5  9674  cantnfle  9708  rankuni  9900  djuunxp  9958  acndom  10088  acnnum  10089  cdainflem  10225  cfcof  10311  ac6num  10516  ac6s2  10523  brdom5  10566  brdom4  10567  genpnnp  11042  divmulasscom  11943  lediv2a  12159  supmul1  12234  infregelb  12249  nn2ge  12290  btwnz  12718  eluz2b2  12960  uz2mulcl  12965  eqreznegel  12973  xrsupexmnf  13343  xrinfmexpnf  13344  xrsupsslem  13345  xrinfmsslem  13346  supxrun  13354  ioo0  13408  elioo4g  13443  fz0fzelfz0  13670  fz0fzdiffz0  13673  2ffzeq  13685  elfzodifsumelfzo  13766  elfzom1elp1fzo  13767  zpnn0elfzo  13773  elfzom1elp1fzo1  13802  fzonfzoufzol  13805  quoremnn0  13892  zmodidfzoimp  13937  modabs  13940  modifeq2int  13970  modaddmulmod  13975  expcl2lem  14110  hashgt23el  14459  hashreshashfun  14474  iswrdsymb  14565  ccatcl  14608  ccatsymb  14616  swrdfv2  14695  swrdsbslen  14698  swrdspsleq  14699  pfxswrd  14740  pfxccatin12lem3  14766  pfxccatpfx2  14771  swrdccat3blem  14773  reuccatpfxs1  14781  repswccat  14820  cshweqdifid  14854  lswco  14874  repsco  14875  s4f1o  14953  trclun  15049  mulre  15156  rediv  15166  imdiv  15173  resqrex  15285  caurcvg2  15710  fsumdifsnconst  15823  modfsummods  15825  tanval  16160  p1modz1  16293  negdvdsb  16306  muldvds1  16314  muldvds2  16315  dvdscmulr  16318  dvdsmulcr  16319  sumodd  16421  divalglem8  16433  divgcdnn  16548  lcmfunsnlem2lem2  16672  lcmfun  16678  2mulprm  16726  maxprmfct  16742  vfermltlALT  16835  modprm0  16838  pcpremul  16876  pcmul  16884  oddprmdvds  16936  prmdvdsprmo  17075  cshwsidrepsw  17127  gsumccat  18866  grpissubg  19176  ecqusaddd  19222  ecqusaddcl  19223  eqg0subg  19226  gim0to0  19299  gsmsymgreqlem2  19463  symgfixfo  19471  fsfnn0gsumfsffz  20015  rnglz  20182  isringrng  20300  irredn0  20439  c0snmgmhm  20478  rimisrngim  20514  zrrnghm  20552  rnghmsubcsetclem2  20648  rhmsubcsetclem2  20677  rhmsubcrngclem2  20683  lsppratlem1  21166  qusmulrng  21309  quscrng  21310  rngqiprngghmlem3  21316  rngqiprnglinlem3  21320  rngqiprngimf1lem  21321  rngqiprnglin  21329  cnfldfunALT  21396  cnfldfunALTOLD  21409  dvdsrzring  21489  mpofrlmd  21814  matinvgcell  22456  mat1dimcrng  22498  dmatscmcl  22524  scmatscm  22534  scmatghm  22554  scmatmhm  22555  ma1repvcl  22591  slesolinv  22701  slesolinvbi  22702  cramerimplem1  22704  cramerimp  22707  cramerlem1  22708  cramer  22712  cpmatacl  22737  cpmatmcl  22740  mat2pmatghm  22751  mat2pmatmul  22752  m2pmfzgsumcl  22769  decpmatmul  22793  decpmatmulsumfsupp  22794  pmatcollpwfi  22803  pm2mpf1  22820  pm2mpghm  22837  pm2mpmhmlem1  22839  monmat2matmon  22845  chpdmatlem2  22860  chpdmat  22862  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  clscld  23070  neiptopnei  23155  2ndcdisj2  23480  comppfsc  23555  tx1stc  23673  opnfbas  23865  fbasfip  23891  alexsublem  24067  alexsubALTlem4  24073  cnextcn  24090  ngpocelbl  24740  cphipval  25290  bcthlem5  25375  vitalilem4  25659  vitalilem5  25660  itg2mulc  25796  bddiblnc  25891  dvcobr  25997  dvcobrOLD  25998  dvcnvlem  26028  dvferm1  26037  dvne0  26064  mdegmullem  26131  plyeq0lem  26263  plyexmo  26369  aalioulem5  26392  aalioulem6  26393  aaliou  26394  cxple2a  26755  cxpaddlelem  26808  cxpaddle  26809  relogbcxpb  26844  bcmono  27335  lgsprme0  27397  gausslemma2dlem0e  27418  gausslemma2dlem1a  27423  gausslemma2dlem6  27430  lgsquadlem2  27439  2lgsoddprm  27474  elno2  27713  cofcutr  27972  colinearalg  28939  axcontlem3  28995  umgrislfupgrlem  29153  edgupgr  29165  usgruspgrb  29214  usgrislfuspgr  29218  edgssv2  29229  umgr2edg  29240  uspgredg2v  29255  usgrexmplef  29290  subupgr  29318  subusgr  29320  nbupgrres  29395  nb3gr2nb  29415  nbupgruvtxres  29438  cusgrres  29480  cusgrsizeindslem  29483  cusgrsizeinds  29484  vtxdun  29513  finrusgrfusgr  29597  cusgrrusgr  29613  spthdep  29766  cycliscrct  29831  crctcshwlkn0lem6  29844  crctcshwlkn0lem7  29845  crctcshtrl  29852  crctcsh  29853  umgr2adedgwlkonALT  29976  elwwlks2  29995  elwspths2spth  29996  rusgrnumwwlk  30004  clwlkclwwlklem2a  30026  clwlkclwwlklem3  30029  clwwisshclwws  30043  wwlksubclwwlk  30086  eleclclwwlknlem2  30089  eupth2lem3lem3  30258  eucrct2eupth1  30272  frgr3v  30303  3vfriswmgr  30306  1to3vfriswmgr  30308  3cyclfrgr  30316  vdgn1frgrv2  30324  frgrwopreglem5  30349  frgrwopreglem5ALT  30350  frrusgrord0lem  30367  frrusgrord0  30368  2clwwlk2clwwlk  30378  extwwlkfab  30380  numclwwlk1lem2fo  30386  friendshipgt3  30426  ex-natded9.20-2  30446  grpoidinvlem3  30534  grpoidinv  30536  nmobndseqi  30807  nmobndseqiALT  30808  hvaddsub4  31106  ocsh  31311  5oalem2  31683  5oalem5  31686  3oalem2  31691  pjjsi  31728  hoadddir  31832  leopmul  32162  stge1i  32266  hatomistici  32390  mdsymlem2  32432  mdsymlem5  32435  addltmulALT  32474  isoun  32716  fsumiunle  32835  lsmsnorb  33398  crefdf  33808  qqhre  33982  esumiun  34074  sxbrsigalem0  34252  dya2iocnei  34263  sxbrsigalem5  34269  sibfinima  34320  eulerpartlemgs2  34361  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemsup  34485  bnj529  34733  bnj945  34765  bnj1098  34775  bnj1533  34844  bnj605  34899  bnj594  34904  bnj607  34908  bnj966  34936  bnj967  34937  bnj996  34948  bnj999  34950  bnj1006  34952  bnj1118  34976  bnj1172  34993  bnj1279  35010  bnj1296  35013  bnj1498  35053  fnrelpredd  35081  lfuhgr3  35103  loop1cycl  35121  cvmsi  35249  satf0op  35361  satffunlem1lem1  35386  satffunlem2lem1  35388  fv2ndcnv  35758  trisegint  36009  funtransport  36012  btwnconn1lem4  36071  btwnconn2  36083  segcon2  36086  outsideofeu  36112  isfne  36321  lukshef-ax2  36397  limsucncmpi  36427  weiunso  36448  bj-nsnid  37052  bj-restn0b  37073  bj-eldiag2  37159  bj-isrvec2  37282  pibt2  37399  unccur  37589  lindsadd  37599  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  poimirlem30  37636  poimirlem32  37638  heicant  37641  ismblfin  37647  itg2gt0cn  37661  areacirc  37699  opelopab3  37704  isdivrngo  37936  isdrngo2  37944  fldcrngo  37990  flddmn  38044  refrelredund4  38616  mainer2  38827  cmtbr4N  39236  linepsubN  39734  pmapsub  39750  paddasslem14  39815  pclcmpatN  39883  trlval2  40145  cdleme20  40306  cdleme21j  40318  dvalveclem  41007  dia2dimlem7  41052  dvhlveclem  41090  docaclN  41106  dihjat1  41411  mapdhcl  41709  mapdh6dN  41721  mapdh8  41770  hdmap1l6d  41795  hdmap10  41822  hdmaprnlem17N  41845  hdmaplkr  41895  hdmapip0  41897  hgmapvv  41908  aks6d1c4  42105  cmpfiiin  42684  pellexlem4  42819  pellqrex  42866  acongtr  42966  acongrep  42968  jm2.23  42984  omlimcl2  43230  onsucf1lem  43258  oege1  43295  nnoeomeqom  43301  cantnfresb  43313  onmcl  43320  tfsconcat0i  43334  ofoafg  43343  ofoafo  43345  ofoaass  43349  ofoacom  43350  naddcnfass  43358  rp-fakeanorass  43502  rp-isfinite6  43507  harval3  43527  inintabss  43567  rfovcnvf1od  43993  clsk1indlem3  44032  ntrclsk13  44060  pm10.55  44364  refsum2cnlem1  44974  axccd2  45172  mptssid  45184  fmuldfeq  45538  climsuse  45563  limclner  45606  climxlim2lem  45800  icccncfext  45842  stoweidlem26  45981  stoweidlem52  46007  stoweidlem57  46012  fourierdlem20  46082  fourierdlem41  46103  fourierdlem52  46113  fourierdlem64  46125  fourierdlem102  46163  fourierdlem114  46175  ovolval4lem1  46604  preimagelt  46654  preimalegt  46655  funressneu  46996  afvelrn  47117  elfz2z  47264  2ffzoeq  47276  zplusmodne  47282  addmodne  47283  minusmod5ne  47288  imasetpreimafvbijlemfv  47326  imasetpreimafvbijlemf1  47328  fargshiftfva  47367  ichreuopeq  47397  2exopprim  47449  reuopreuprim  47450  fmtnoprmfac1  47489  proththd  47538  opoeALTV  47607  evensumeven  47631  sbgoldbalt  47705  evengpop3  47722  evengpoap3  47723  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  tgoldbach  47741  dfclnbgr6  47779  dfsclnbgr6  47781  uspgrimprop  47810  isuspgrimlem  47811  gricushgr  47823  uhgrimisgrgric  47836  isubgr3stgrlem7  47874  uspgrlimlem2  47891  gpgedgvtx0  47953  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem3  47963  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  gpg5gricstgr3  47973  assintop  48052  uzlidlring  48078  2zrngnmrid  48099  cznrng  48104  lmodvsmdi  48223  lincsum  48274  lincsumcl  48276  el0ldep  48311  ldepspr  48318  lindssnlvec  48331  modn0mul  48369  m1modmmod  48370  nn0digval  48449  1arympt1fv  48488  eenglngeehlnmlem1  48586  rrx2linest  48591  line2  48601  itsclc0yqe  48610  r19.41dv  48650  setrec1lem3  48919  aacllem  49031