Theorem anim1i 621

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sylanl1  686  sylanr1  688  eu6im  2579  r19.28v  3171  rmob  3829  eqeuel  4300  preq12nebg  4801  fores  6756  fdmeu  6890  ssimaex  6919  dffv2  6929  exfo  7053  fpropnf1  7218  f1ocoima  7254  oprabv  7423  ndmovass  7551  fun11uni  7880  resf1ext2b  7882  fabexgOLD  7886  f1oabexgOLD  7890  f1iun  7893  soxp  8076  tz7.48lem  8377  tz7.49c  8382  omass  8512  oewordri  8525  omabs  8584  sbthlem9  9030  pssnn  9100  fineqvlem  9173  domunfican  9229  fiint  9234  fsuppsssupp  9291  sup0  9377  inf1  9541  infeq5  9556  cantnfle  9590  rankuni  9785  djuunxp  9843  acndom  9971  acnnum  9972  cdainflem  10108  cfcof  10194  ac6num  10399  ac6s2  10406  brdom5  10449  brdom4  10450  genpnnp  10926  divmulasscom  11831  lediv2a  12048  supmul1  12123  infregelb  12138  nn2ge  12202  btwnz  12630  eluz2b2  12869  uz2mulcl  12874  eqreznegel  12882  xrsupexmnf  13255  xrinfmexpnf  13256  xrsupsslem  13257  xrinfmsslem  13258  supxrun  13266  ioo0  13321  elioo4g  13357  fz0fzelfz0  13586  fz0fzdiffz0  13589  2ffzeq  13601  elfzodifsumelfzo  13684  elfzom1elp1fzo  13685  zpnn0elfzo  13691  elfzom1elp1fzo1  13720  fzonfzoufzol  13724  quoremnn0  13813  zmodidfzoimp  13858  modabs  13861  modaddb  13866  modifeq2int  13893  modaddmulmod  13898  expcl2lem  14033  hashgt23el  14384  hashreshashfun  14399  iswrdsymb  14491  ccatcl  14534  ccatsymb  14543  swrdfv2  14622  swrdsbslen  14625  swrdspsleq  14626  pfxswrd  14666  pfxccatin12lem3  14692  pfxccatpfx2  14697  swrdccat3blem  14699  reuccatpfxs1  14707  repswccat  14746  cshweqdifid  14780  lswco  14799  repsco  14800  s4f1o  14878  trclun  14974  mulre  15081  rediv  15091  imdiv  15098  resqrex  15210  caurcvg2  15638  fsumdifsnconst  15752  modfsummods  15754  tanval  16093  p1modz1  16226  negdvdsb  16239  muldvds1  16247  muldvds2  16248  dvdscmulr  16251  dvdsmulcr  16252  sumodd  16355  divalglem8  16367  divgcdnn  16482  lcmfunsnlem2lem2  16606  lcmfun  16612  2mulprm  16660  maxprmfct  16677  vfermltlALT  16771  modprm0  16774  pcpremul  16812  pcmul  16820  oddprmdvds  16872  prmdvdsprmo  17011  cshwsidrepsw  17062  gsumccat  18807  grpissubg  19120  ecqusaddd  19165  ecqusaddcl  19166  eqg0subg  19169  gim0to0  19242  gsmsymgreqlem2  19404  symgfixfo  19412  fsfnn0gsumfsffz  19956  rnglz  20144  isringrng  20266  irredn0  20401  c0snmgmhm  20440  rimisrngim  20476  zrrnghm  20515  rnghmsubcsetclem2  20611  rhmsubcsetclem2  20640  rhmsubcrngclem2  20646  lsppratlem1  21147  qusmulrng  21282  quscrng  21283  rngqiprngghmlem3  21289  rngqiprnglinlem3  21293  rngqiprngimf1lem  21294  rngqiprnglin  21302  cnfldfunALT  21369  dvdsrzring  21443  mpofrlmd  21759  matinvgcell  22425  mat1dimcrng  22467  dmatscmcl  22493  scmatscm  22503  scmatghm  22523  scmatmhm  22524  ma1repvcl  22560  slesolinv  22670  slesolinvbi  22671  cramerimplem1  22673  cramerimp  22676  cramerlem1  22677  cramer  22681  cpmatacl  22706  cpmatmcl  22709  mat2pmatghm  22720  mat2pmatmul  22721  m2pmfzgsumcl  22738  decpmatmul  22762  decpmatmulsumfsupp  22763  pmatcollpwfi  22772  pm2mpf1  22789  pm2mpghm  22806  pm2mpmhmlem1  22808  monmat2matmon  22814  chpdmatlem2  22829  chpdmat  22831  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  clscld  23037  neiptopnei  23122  2ndcdisj2  23447  comppfsc  23522  tx1stc  23640  opnfbas  23832  fbasfip  23858  alexsublem  24034  alexsubALTlem4  24040  cnextcn  24057  ngpocelbl  24694  cphipval  25235  bcthlem5  25320  vitalilem4  25603  vitalilem5  25604  itg2mulc  25739  bddiblnc  25834  dvcobr  25938  dvcnvlem  25968  dvferm1  25977  dvne0  26003  mdegmullem  26068  plyeq0lem  26200  plyexmo  26304  aalioulem5  26327  aalioulem6  26328  aaliou  26329  cxple2a  26688  cxpaddlelem  26740  cxpaddle  26741  relogbcxpb  26776  bcmono  27265  lgsprme0  27327  gausslemma2dlem0e  27348  gausslemma2dlem1a  27353  gausslemma2dlem6  27360  lgsquadlem2  27369  2lgsoddprm  27404  elno2  27643  cofcutr  27941  colinearalg  29004  axcontlem3  29060  umgrislfupgrlem  29216  edgupgr  29228  usgruspgrb  29277  usgrislfuspgr  29281  edgssv2  29292  umgr2edg  29303  uspgredg2v  29318  usgrexmplef  29353  subupgr  29381  subusgr  29383  nbupgrres  29458  nb3gr2nb  29478  nbupgruvtxres  29501  cusgrres  29542  cusgrsizeindslem  29545  cusgrsizeinds  29546  vtxdun  29575  finrusgrfusgr  29659  cusgrrusgr  29675  pthdifv  29823  spthdep  29827  cycliscrct  29892  crctcshwlkn0lem6  29908  crctcshwlkn0lem7  29909  crctcshtrl  29916  crctcsh  29917  umgr2adedgwlkonALT  30040  elwwlks2  30062  elwspths2spth  30063  rusgrnumwwlk  30071  clwlkclwwlklem2a  30093  clwlkclwwlklem3  30096  clwwisshclwws  30110  wwlksubclwwlk  30153  eleclclwwlknlem2  30156  eupth2lem3lem3  30325  eucrct2eupth1  30339  frgr3v  30370  3vfriswmgr  30373  1to3vfriswmgr  30375  3cyclfrgr  30383  vdgn1frgrv2  30391  frgrwopreglem5  30416  frgrwopreglem5ALT  30417  frrusgrord0lem  30434  frrusgrord0  30435  2clwwlk2clwwlk  30445  extwwlkfab  30447  numclwwlk1lem2fo  30453  friendshipgt3  30493  ex-natded9.20-2  30513  grpoidinvlem3  30602  grpoidinv  30604  nmobndseqi  30875  nmobndseqiALT  30876  hvaddsub4  31174  ocsh  31379  5oalem2  31751  5oalem5  31754  3oalem2  31759  pjjsi  31796  hoadddir  31900  leopmul  32230  stge1i  32334  hatomistici  32458  mdsymlem2  32500  mdsymlem5  32503  addltmulALT  32542  isoun  32801  fsumiunle  32928  lsmsnorb  33481  crefdf  34039  qqhre  34211  esumiun  34285  sxbrsigalem0  34462  dya2iocnei  34473  sxbrsigalem5  34479  sibfinima  34530  eulerpartlemgs2  34571  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemsup  34696  bnj529  34931  bnj945  34963  bnj1098  34973  bnj1533  35041  bnj605  35096  bnj594  35101  bnj607  35105  bnj966  35133  bnj967  35134  bnj996  35145  bnj999  35147  bnj1006  35149  bnj1118  35173  bnj1172  35190  bnj1279  35207  bnj1296  35210  bnj1498  35250  fnrelpredd  35279  lfuhgr3  35355  loop1cycl  35372  cvmsi  35500  satf0op  35612  satffunlem1lem1  35637  satffunlem2lem1  35639  fv2ndcnv  36013  trisegint  36263  funtransport  36266  btwnconn1lem4  36325  btwnconn2  36337  segcon2  36340  outsideofeu  36366  isfne  36574  lukshef-ax2  36650  limsucncmpi  36680  weiunso  36701  bj-nsnid  37430  bj-restn0b  37456  bj-eldiag2  37544  bj-isrvec2  37667  pibt2  37786  unccur  37977  lindsadd  37987  lindsenlbs  37989  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem26  38020  poimirlem27  38021  poimirlem29  38023  poimirlem30  38024  poimirlem32  38026  heicant  38029  ismblfin  38035  itg2gt0cn  38049  areacirc  38087  opelopab3  38092  isdivrngo  38324  isdrngo2  38332  fldcrngo  38378  flddmn  38432  refrelredund4  39093  mainer2  39334  cmtbr4N  39754  linepsubN  40251  pmapsub  40267  paddasslem14  40332  pclcmpatN  40400  trlval2  40662  cdleme20  40823  cdleme21j  40835  dvalveclem  41524  dia2dimlem7  41569  dvhlveclem  41607  docaclN  41623  dihjat1  41928  mapdhcl  42226  mapdh6dN  42238  mapdh8  42287  hdmap1l6d  42312  hdmap10  42339  hdmaprnlem17N  42362  hdmaplkr  42412  hdmapip0  42414  hgmapvv  42425  aks6d1c4  42616  cmpfiiin  43153  pellexlem4  43284  pellqrex  43331  acongtr  43430  acongrep  43432  jm2.23  43448  omlimcl2  43694  onsucf1lem  43721  oege1  43758  nnoeomeqom  43764  cantnfresb  43776  onmcl  43783  tfsconcat0i  43797  ofoafg  43806  ofoafo  43808  ofoaass  43812  ofoacom  43813  naddcnfass  43821  rp-fakeanorass  43964  rp-isfinite6  43969  harval3  43989  inintabss  44029  rfovcnvf1od  44455  clsk1indlem3  44494  ntrclsk13  44522  pm10.55  44820  refsum2cnlem1  45492  axccd2  45681  mptssid  45692  fmuldfeq  46035  climsuse  46060  limclner  46101  climxlim2lem  46295  icccncfext  46337  stoweidlem26  46476  stoweidlem52  46502  stoweidlem57  46507  fourierdlem20  46577  fourierdlem41  46598  fourierdlem52  46608  fourierdlem64  46620  fourierdlem102  46658  fourierdlem114  46670  ovolval4lem1  47099  preimagelt  47149  preimalegt  47150  squeezedltsq  47340  funressneu  47517  afvelrn  47638  elfz2z  47785  2ffzoeq  47798  zplusmodne  47819  addmodne  47820  minusmod5ne  47825  modn0mul  47833  m1modmmod  47834  nndivides2  47854  imasetpreimafvbijlemfv  47884  imasetpreimafvbijlemf1  47886  fargshiftfva  47925  ichreuopeq  47955  2exopprim  48007  reuopreuprim  48008  fmtnoprmfac1  48050  proththd  48099  opoeALTV  48181  evensumeven  48205  sbgoldbalt  48279  evengpop3  48296  evengpoap3  48297  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  wtgoldbnnsum4prm  48300  bgoldbnnsum3prm  48302  tgoldbach  48315  dfclnbgr6  48354  dfsclnbgr6  48356  uhgrimedg  48389  uhgrimprop  48390  isuspgrimlem  48393  isuspgrim  48394  gricushgr  48415  uhgrimisgrgric  48429  isubgr3stgrlem7  48470  uspgrlimlem2  48487  gpgedgel  48548  gpgprismgriedgdmss  48550  gpgedgvtx0  48559  gpgedgiov  48563  gpgedg2ov  48564  gpgedg2iv  48565  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem3  48571  gpg5nbgrvtx03star  48578  gpg5nbgr3star  48579  gpg5gricstgr3  48588  pgnbgreunbgrlem4  48617  assintop  48707  uzlidlring  48733  2zrngnmrid  48754  cznrng  48759  lmodvsmdi  48877  lincsum  48927  lincsumcl  48929  el0ldep  48964  ldepspr  48971  lindssnlvec  48984  nn0digval  49098  1arympt1fv  49137  eenglngeehlnmlem1  49235  rrx2linest  49240  line2  49250  itsclc0yqe  49259  r19.41dv  49299  setrec1lem3  50186  aacllem  50298