Theorem anim1i 624

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sylanl1  690  sylanr1  692  eu6im  2601  r19.28v  3192  rmob  3843  eqeuel  4317  preq12nebg  4820  fores  6784  fdmeu  6919  ssimaex  6948  dffv2  6958  exfo  7082  fpropnf1  7247  f1ocoima  7283  oprabv  7452  ndmovass  7580  fun11uni  7910  resf1ext2b  7912  f1iun  7921  soxp  8104  tz7.48lem  8407  tz7.49c  8412  omass  8544  oewordri  8557  omabs  8616  sbthlem9  9063  pssnn  9133  fineqvlem  9206  domunfican  9262  fiint  9267  fsuppsssupp  9324  sup0  9410  inf1  9574  infeq5  9589  cantnfle  9623  rankuni  9818  djuunxp  9876  acndom  10004  acnnum  10005  cdainflem  10141  cfcof  10228  ac6num  10433  ac6s2  10440  brdom5  10483  brdom4  10484  genpnnp  10960  divmulasscom  11866  lediv2a  12083  supmul1  12158  infregelb  12173  nn2ge  12237  btwnz  12673  eluz2b2  12919  uz2mulcl  12924  eqreznegel  12932  xrsupexmnf  13305  xrinfmexpnf  13306  xrsupsslem  13307  xrinfmsslem  13308  supxrun  13316  ioo0  13371  elioo4g  13407  fz0fzelfz0  13636  fz0fzdiffz0  13639  2ffzeq  13651  elfzodifsumelfzo  13734  elfzom1elp1fzo  13735  zpnn0elfzo  13741  elfzom1elp1fzo1  13770  fzonfzoufzol  13774  quoremnn0  13863  zmodidfzoimp  13908  modabs  13911  modaddb  13916  modifeq2int  13943  modaddmulmod  13948  expcl2lem  14083  hashgt23el  14434  hashreshashfun  14449  iswrdsymb  14541  ccatcl  14584  ccatsymb  14593  swrdfv2  14672  swrdsbslen  14675  swrdspsleq  14676  pfxswrd  14716  pfxccatin12lem3  14742  pfxccatpfx2  14747  swrdccat3blem  14749  reuccatpfxs1  14757  repswccat  14796  cshweqdifid  14830  lswco  14849  repsco  14850  s4f1o  14928  trclun  15024  mulre  15131  rediv  15141  imdiv  15148  resqrex  15260  caurcvg2  15688  fsumdifsnconst  15802  modfsummods  15804  tanval  16143  p1modz1  16276  negdvdsb  16289  muldvds1  16297  muldvds2  16298  dvdscmulr  16301  dvdsmulcr  16302  sumodd  16405  divalglem8  16417  divgcdnn  16532  lcmfunsnlem2lem2  16656  lcmfun  16662  2mulprm  16710  maxprmfct  16727  vfermltlALT  16821  modprm0  16824  pcpremul  16862  pcmul  16870  oddprmdvds  16922  prmdvdsprmo  17061  cshwsidrepsw  17112  gsumccat  18858  grpissubg  19171  ecqusaddd  19216  ecqusaddcl  19217  eqg0subg  19220  gim0to0  19292  gsmsymgreqlem2  19454  symgfixfo  19462  fsfnn0gsumfsffz  20006  rnglz  20194  isringrng  20316  irredn0  20451  c0snmgmhm  20490  rimisrngim  20526  zrrnghm  20565  rnghmsubcsetclem2  20661  rhmsubcsetclem2  20690  rhmsubcrngclem2  20696  lsppratlem1  21197  qusmulrng  21332  quscrng  21333  rngqiprngghmlem3  21339  rngqiprnglinlem3  21343  rngqiprngimf1lem  21344  rngqiprnglin  21352  cnfldfunALT  21419  dvdsrzring  21493  mpofrlmd  21809  matinvgcell  22475  mat1dimcrng  22517  dmatscmcl  22543  scmatscm  22553  scmatghm  22573  scmatmhm  22574  ma1repvcl  22610  slesolinv  22720  slesolinvbi  22721  cramerimplem1  22723  cramerimp  22726  cramerlem1  22727  cramer  22731  cpmatacl  22756  cpmatmcl  22759  mat2pmatghm  22770  mat2pmatmul  22771  m2pmfzgsumcl  22788  decpmatmul  22812  decpmatmulsumfsupp  22813  pmatcollpwfi  22822  pm2mpf1  22839  pm2mpghm  22856  pm2mpmhmlem1  22858  monmat2matmon  22864  chpdmatlem2  22879  chpdmat  22881  cpmadugsumlemB  22914  cpmadugsumlemC  22915  cpmadugsumlemF  22916  clscld  23087  neiptopnei  23172  2ndcdisj2  23497  comppfsc  23572  tx1stc  23690  opnfbas  23882  fbasfip  23908  alexsublem  24084  alexsubALTlem4  24090  cnextcn  24107  ngpocelbl  24744  cphipval  25285  bcthlem5  25370  vitalilem4  25653  vitalilem5  25654  itg2mulc  25789  bddiblnc  25884  dvcobr  25988  dvcnvlem  26018  dvferm1  26027  dvne0  26053  mdegmullem  26118  plyeq0lem  26250  plyexmo  26354  aalioulem5  26377  aalioulem6  26378  aaliou  26379  cxple2a  26741  cxpaddlelem  26793  cxpaddle  26794  relogbcxpb  26829  bcmono  27318  lgsprme0  27380  gausslemma2dlem0e  27401  gausslemma2dlem1a  27406  gausslemma2dlem6  27413  lgsquadlem2  27422  2lgsoddprm  27457  elno2  27695  cofcutr  27994  colinearalg  29057  axcontlem3  29113  umgrislfupgrlem  29269  edgupgr  29281  usgruspgrb  29330  usgrislfuspgr  29334  edgssv2  29345  umgr2edg  29356  uspgredg2v  29371  usgrexmplef  29406  subupgr  29434  subusgr  29436  nbupgrres  29511  nb3gr2nb  29531  nbupgruvtxres  29554  cusgrres  29595  cusgrsizeindslem  29598  cusgrsizeinds  29599  vtxdun  29628  finrusgrfusgr  29712  cusgrrusgr  29728  pthdifv  29876  spthdep  29880  cycliscrct  29945  crctcshwlkn0lem6  29961  crctcshwlkn0lem7  29962  crctcshtrl  29969  crctcsh  29970  umgr2adedgwlkonALT  30093  elwwlks2  30115  elwspths2spth  30116  rusgrnumwwlk  30124  clwlkclwwlklem2a  30146  clwlkclwwlklem3  30149  clwwisshclwws  30163  wwlksubclwwlk  30206  eleclclwwlknlem2  30209  eupth2lem3lem3  30378  eucrct2eupth1  30392  frgr3v  30423  3vfriswmgr  30426  1to3vfriswmgr  30428  3cyclfrgr  30436  vdgn1frgrv2  30444  frgrwopreglem5  30469  frgrwopreglem5ALT  30470  frrusgrord0lem  30487  frrusgrord0  30488  2clwwlk2clwwlk  30498  extwwlkfab  30500  numclwwlk1lem2fo  30506  friendshipgt3  30546  ex-natded9.20-2  30566  grpoidinvlem3  30655  grpoidinv  30657  nmobndseqi  30928  nmobndseqiALT  30929  hvaddsub4  31227  ocsh  31432  5oalem2  31804  5oalem5  31807  3oalem2  31812  pjjsi  31849  hoadddir  31953  leopmul  32283  stge1i  32387  hatomistici  32511  mdsymlem2  32553  mdsymlem5  32556  addltmulALT  32595  isoun  32854  fsumiunle  32981  lsmsnorb  33538  crefdf  34106  qqhre  34278  esumiun  34352  sxbrsigalem0  34529  dya2iocnei  34540  sxbrsigalem5  34546  sibfinima  34597  eulerpartlemgs2  34638  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemsup  34763  bnj529  35001  bnj945  35033  bnj1098  35043  bnj1533  35111  bnj605  35166  bnj594  35171  bnj607  35175  bnj966  35203  bnj967  35204  bnj996  35215  bnj999  35217  bnj1006  35219  bnj1118  35243  bnj1172  35260  bnj1279  35277  bnj1296  35280  bnj1498  35320  fnrelpredd  35351  lfuhgr3  35434  loop1cycl  35451  cvmsi  35579  satf0op  35691  satffunlem1lem1  35716  satffunlem2lem1  35718  fv2ndcnv  36092  trisegint  36342  funtransport  36345  btwnconn1lem4  36404  btwnconn2  36416  segcon2  36419  outsideofeu  36445  isfne  36663  lukshef-ax2  36739  limsucncmpi  36769  weiunso  36790  bj-nsnid  37519  bj-restn0b  37545  bj-eldiag2  37633  bj-isrvec2  37756  pibt2  37875  unccur  38066  lindsadd  38076  lindsenlbs  38078  matunitlindflem1  38079  matunitlindflem2  38080  poimirlem26  38109  poimirlem27  38110  poimirlem29  38112  poimirlem30  38113  poimirlem32  38115  heicant  38118  ismblfin  38124  itg2gt0cn  38138  areacirc  38176  opelopab3  38181  isdivrngo  38413  isdrngo2  38421  fldcrngo  38467  flddmn  38521  refrelredund4  39182  mainer2  39423  cmtbr4N  39843  linepsubN  40340  pmapsub  40356  paddasslem14  40421  pclcmpatN  40489  trlval2  40751  cdleme20  40912  cdleme21j  40924  dvalveclem  41613  dia2dimlem7  41658  dvhlveclem  41696  docaclN  41712  dihjat1  42017  mapdhcl  42315  mapdh6dN  42327  mapdh8  42376  hdmap1l6d  42401  hdmap10  42428  hdmaprnlem17N  42451  hdmaplkr  42501  hdmapip0  42503  hgmapvv  42514  aks6d1c4  42705  cmpfiiin  43242  pellexlem4  43373  pellqrex  43420  acongtr  43519  acongrep  43521  jm2.23  43537  omlimcl2  43783  onsucf1lem  43810  oege1  43847  nnoeomeqom  43853  cantnfresb  43865  onmcl  43872  tfsconcat0i  43886  ofoafg  43895  ofoafo  43897  ofoaass  43901  ofoacom  43902  naddcnfass  43910  rp-fakeanorass  44053  rp-isfinite6  44058  harval3  44078  inintabss  44118  rfovcnvf1od  44544  clsk1indlem3  44583  ntrclsk13  44611  pm10.55  44909  refsum2cnlem1  45581  axccd2  45769  mptssid  45780  fmuldfeq  46123  climsuse  46148  limclner  46189  climxlim2lem  46383  icccncfext  46425  stoweidlem26  46564  stoweidlem52  46590  stoweidlem57  46595  fourierdlem20  46665  fourierdlem41  46686  fourierdlem52  46696  fourierdlem64  46708  fourierdlem102  46746  fourierdlem114  46758  ovolval4lem1  47187  preimagelt  47237  preimalegt  47238  squeezedltsq  47428  funressneu  47605  afvelrn  47726  elfz2z  47873  2ffzoeq  47886  zplusmodne  47907  addmodne  47908  minusmod5ne  47913  modn0mul  47921  m1modmmod  47922  nndivides2  47942  imasetpreimafvbijlemfv  47972  imasetpreimafvbijlemf1  47974  fargshiftfva  48013  ichreuopeq  48043  2exopprim  48095  reuopreuprim  48096  fmtnoprmfac1  48138  proththd  48187  opoeALTV  48269  evensumeven  48293  sbgoldbalt  48367  evengpop3  48384  evengpoap3  48385  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  wtgoldbnnsum4prm  48388  bgoldbnnsum3prm  48390  tgoldbach  48403  dfclnbgr6  48442  dfsclnbgr6  48444  uhgrimedg  48477  uhgrimprop  48478  isuspgrimlem  48481  isuspgrim  48482  gricushgr  48503  uhgrimisgrgric  48517  isubgr3stgrlem7  48558  uspgrlimlem2  48575  gpgedgel  48636  gpgprismgriedgdmss  48638  gpgedgvtx0  48647  gpgedgiov  48651  gpgedg2ov  48652  gpgedg2iv  48653  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem3  48659  gpg5nbgrvtx03star  48666  gpg5nbgr3star  48667  gpg5gricstgr3  48676  pgnbgreunbgrlem4  48705  assintop  48795  uzlidlring  48821  2zrngnmrid  48842  cznrng  48847  lmodvsmdi  48965  lincsum  49015  lincsumcl  49017  el0ldep  49052  ldepspr  49059  lindssnlvec  49072  nn0digval  49186  1arympt1fv  49225  eenglngeehlnmlem1  49323  rrx2linest  49328  line2  49338  itsclc0yqe  49347  r19.41dv  49387  setrec1lem3  50274  aacllem  50386