Theorem anim1i 627

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 23	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	anim12i 625	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylanl1  693  sylanr1  695  eu6im  2606  r19.28v  3199  rmob  3846  eqeuel  4323  preq12nebg  4833  fores  6809  fdmeu  6944  ssimaex  6973  dffv2  6983  exfo  7107  fpropnf1  7272  f1ocoima  7312  oprabv  7483  ndmovass  7611  fun11uni  7939  resf1ext2b  7941  f1iun  7950  soxp  8134  tz7.48lem  8437  tz7.49c  8442  omass  8574  oewordri  8587  omabs  8646  sbthlem9  9093  pssnn  9163  fineqvlem  9236  domunfican  9291  fiint  9296  fsuppsssupp  9351  sup0  9437  inf1  9601  infeq5  9616  cantnfle  9650  rankuni  9845  djuunxp  9926  acndom  10054  acnnum  10055  cdainflem  10190  cfcof  10276  ac6num  10481  ac6s2  10488  brdom5  10531  brdom4  10532  genpnnp  11008  divmulasscom  11914  lediv2a  12127  supmul1  12202  infregelb  12217  nn2ge  12281  btwnz  12717  eluz2b2  12963  uz2mulcl  12968  eqreznegel  12976  xrsupexmnf  13349  xrinfmexpnf  13350  xrsupsslem  13351  xrinfmsslem  13352  supxrun  13360  ioo0  13415  elioo4g  13451  fz0fzelfz0  13681  fz0fzdiffz0  13684  2ffzeq  13696  elfzodifsumelfzo  13779  elfzom1elp1fzo  13780  zpnn0elfzo  13786  elfzom1elp1fzo1  13815  fzonfzoufzol  13819  quoremnn0  13909  zmodidfzoimp  13954  modabs  13957  modaddb  13962  modifeq2int  13989  modaddmulmod  13994  expcl2lem  14129  hashgt23el  14481  hashreshashfun  14496  iswrdsymb  14588  ccatcl  14631  ccatsymb  14640  swrdfv2  14723  swrdsbslen  14726  swrdspsleq  14727  pfxswrd  14767  pfxccatin12lem3  14793  pfxccatpfx2  14798  swrdccat3blem  14800  reuccatpfxs1  14808  repswccat  14849  cshweqdifid  14883  lswco  14902  repsco  14903  s4f1o  14981  trclun  15077  mulre  15198  rediv  15208  imdiv  15215  resqrex  15327  caurcvg2  15755  fsumdifsnconst  15869  modfsummods  15871  tanval  16209  p1modz1  16342  negdvdsb  16355  muldvds1  16363  muldvds2  16364  dvdscmulr  16367  dvdsmulcr  16368  sumodd  16471  divalglem8  16483  divgcdnn  16598  lcmfunsnlem2lem2  16722  lcmfun  16728  2mulprm  16776  maxprmfct  16793  vfermltlALT  16887  modprm0  16890  pcpremul  16928  pcmul  16936  oddprmdvds  16988  prmdvdsprmo  17127  cshwsidrepsw  17178  gsumccat  18931  grpissubg  19244  ecqusaddd  19294  ecqusaddcl  19295  eqg0subg  19298  gim0to0  19370  gsmsymgreqlem2  19532  symgfixfo  19540  fsfnn0gsumfsffz  20084  rnglz  20274  isringrng  20402  irredn0  20538  c0snmgmhm  20577  rimisrngim  20620  zrrnghm  20672  rnghmsubcsetclem2  20768  rhmsubcsetclem2  20797  rhmsubcrngclem2  20803  lsppratlem1  21308  qusmulrng  21459  quscrng  21460  rngqiprngghmlem3  21466  rngqiprnglinlem3  21470  rngqiprngimf1lem  21471  rngqiprnglin  21479  cnfldfunALT  21574  dvdsrzring  21648  mpofrlmd  21964  matinvgcell  22629  mat1dimcrng  22671  dmatscmcl  22697  scmatscm  22707  scmatghm  22727  scmatmhm  22728  ma1repvcl  22764  slesolinv  22874  slesolinvbi  22875  cramerimplem1  22877  cramerimp  22880  cramerlem1  22881  cramer  22885  cpmatacl  22910  cpmatmcl  22913  mat2pmatghm  22924  mat2pmatmul  22925  m2pmfzgsumcl  22942  decpmatmul  22966  decpmatmulsumfsupp  22967  pmatcollpwfi  22976  pm2mpf1  22993  pm2mpghm  23010  pm2mpmhmlem1  23012  monmat2matmon  23018  chpdmatlem2  23033  chpdmat  23035  cpmadugsumlemB  23068  cpmadugsumlemC  23069  cpmadugsumlemF  23070  clscld  23241  neiptopnei  23326  2ndcdisj2  23651  comppfsc  23726  tx1stc  23844  opnfbas  24036  fbasfip  24062  alexsublem  24238  alexsubALTlem4  24244  cnextcn  24261  ngpocelbl  24898  cphipval  25439  bcthlem5  25524  vitalilem4  25807  vitalilem5  25808  itg2mulc  25943  bddiblnc  26038  dvcobr  26142  dvcnvlem  26172  dvferm1  26181  dvne0  26207  mdegmullem  26272  plyeq0lem  26404  plyexmo  26511  aalioulem5  26536  aalioulem6  26537  aaliou  26538  cxple2a  26901  cxpaddlelem  26953  cxpaddle  26954  relogbcxpb  26989  bcmono  27478  lgsprme0  27540  gausslemma2dlem0e  27561  gausslemma2dlem1a  27566  gausslemma2dlem6  27573  lgsquadlem2  27582  2lgsoddprm  27617  elno2  27855  cofcutr  28154  colinearalg  29297  axcontlem3  29353  umgrislfupgrlem  29509  edgupgr  29521  usgruspgrb  29570  usgrislfuspgr  29574  edgssv2  29585  umgr2edg  29596  uspgredg2v  29611  usgrexmplef  29646  subupgr  29674  subusgr  29676  nbupgrres  29751  nb3gr2nb  29771  nbupgruvtxres  29794  cusgrres  29835  cusgrsizeindslem  29838  cusgrsizeinds  29839  vtxdun  29868  finrusgrfusgr  29952  cusgrrusgr  29968  pthdifv  30116  spthdep  30120  cycliscrct  30185  crctcshwlkn0lem6  30201  crctcshwlkn0lem7  30202  crctcshtrl  30209  crctcsh  30210  umgr2adedgwlkonALT  30333  elwwlks2  30355  elwspths2spth  30356  rusgrnumwwlk  30364  clwlkclwwlklem2a  30386  clwlkclwwlklem3  30389  clwwisshclwws  30403  wwlksubclwwlk  30446  eleclclwwlknlem2  30449  eupth2lem3lem3  30618  eucrct2eupth1  30632  frgr3v  30663  3vfriswmgr  30666  1to3vfriswmgr  30668  3cyclfrgr  30676  vdgn1frgrv2  30684  frgrwopreglem5  30709  frgrwopreglem5ALT  30710  frrusgrord0lem  30727  frrusgrord0  30728  2clwwlk2clwwlk  30738  extwwlkfab  30740  numclwwlk1lem2fo  30746  friendshipgt3  30786  ex-natded9.20-2  30806  grpoidinvlem3  30895  grpoidinv  30897  nmobndseqi  31168  nmobndseqiALT  31169  hvaddsub4  31467  ocsh  31672  5oalem2  32044  5oalem5  32047  3oalem2  32052  pjjsi  32089  hoadddir  32193  leopmul  32523  stge1i  32627  hatomistici  32751  mdsymlem2  32793  mdsymlem5  32796  addltmulALT  32835  isoun  33084  fsumiunle  33210  lsmsnorb  33735  crefdf  34269  qqhre  34441  esumiun  34515  sxbrsigalem0  34692  dya2iocnei  34703  sxbrsigalem5  34709  sibfinima  34760  eulerpartlemgs2  34801  ballotlemfc0  34914  ballotlemfcc  34915  ballotlemsup  34926  bnj529  35161  bnj945  35193  bnj1098  35203  bnj1533  35271  bnj605  35326  bnj594  35331  bnj607  35335  bnj966  35363  bnj967  35364  bnj996  35375  bnj999  35377  bnj1006  35379  bnj1118  35403  bnj1172  35420  bnj1279  35437  bnj1296  35440  bnj1498  35480  fnrelpredd  35506  lfuhgr3  35632  loop1cycl  35649  cvmsi  35777  satf0op  35889  satffunlem1lem1  35914  satffunlem2lem1  35916  fv2ndcnv  36290  trisegint  36540  funtransport  36543  btwnconn1lem4  36602  btwnconn2  36614  segcon2  36617  outsideofeu  36643  isfne  36890  lukshef-ax2  36966  limsucncmpi  36996  weiunso  37017  bj-nsnid  37746  bj-restn0b  37773  bj-eldiag2  37861  bj-isrvec2  37984  pibt2  38103  unccur  38294  lindsadd  38304  lindsenlbs  38306  matunitlindflem1  38307  matunitlindflem2  38308  poimirlem26  38337  poimirlem27  38338  poimirlem29  38340  poimirlem30  38341  poimirlem32  38343  heicant  38346  ismblfin  38352  itg2gt0cn  38366  areacirc  38404  opelopab3  38409  isdivrngo  38641  isdrngo2  38649  fldcrngo  38695  flddmn  38749  refrelredund4  39408  mainer2  39649  cmtbr4N  40069  linepsubN  40566  pmapsub  40582  paddasslem14  40647  pclcmpatN  40715  trlval2  40977  cdleme20  41138  cdleme21j  41150  dvalveclem  41839  dia2dimlem7  41884  dvhlveclem  41922  docaclN  41938  dihjat1  42243  mapdhcl  42541  mapdh6dN  42553  mapdh8  42602  hdmap1l6d  42627  hdmap10  42654  hdmaprnlem17N  42677  hdmaplkr  42727  hdmapip0  42729  hgmapvv  42740  aks6d1c4  42931  cmpfiiin  43468  pellexlem4  43599  pellqrex  43646  acongtr  43745  acongrep  43747  jm2.23  43763  omlimcl2  44009  onsucf1lem  44036  oege1  44073  nnoeomeqom  44079  cantnfresb  44091  onmcl  44098  tfsconcat0i  44112  ofoafg  44121  ofoafo  44123  ofoaass  44127  ofoacom  44128  naddcnfass  44136  rp-fakeanorass  44279  rp-isfinite6  44284  harval3  44304  inintabss  44344  rfovcnvf1od  44770  clsk1indlem3  44809  ntrclsk13  44837  pm10.55  45119  refsum2cnlem1  45797  axccd2  45985  mptssid  45996  fmuldfeq  46339  climsuse  46364  limclner  46405  climxlim2lem  46599  icccncfext  46641  stoweidlem26  46780  stoweidlem52  46806  stoweidlem57  46811  fourierdlem20  46881  fourierdlem41  46902  fourierdlem52  46912  fourierdlem64  46924  fourierdlem102  46962  fourierdlem114  46974  ovolval4lem1  47403  preimagelt  47453  preimalegt  47454  squeezedltsq  47643  funressneu  47824  afvelrn  47945  elfz2z  48092  2ffzoeq  48105  zplusmodne  48126  addmodne  48127  minusmod5ne  48132  modn0mul  48140  m1modmmod  48141  nndivides2  48161  imasetpreimafvbijlemfv  48191  imasetpreimafvbijlemf1  48193  fargshiftfva  48232  ichreuopeq  48262  2exopprim  48314  reuopreuprim  48315  fmtnoprmfac1  48357  proththd  48406  opoeALTV  48488  evensumeven  48512  sbgoldbalt  48586  evengpop3  48603  evengpoap3  48604  nnsum4primeseven  48605  nnsum4primesevenALTV  48606  wtgoldbnnsum4prm  48607  bgoldbnnsum3prm  48609  tgoldbach  48622  dfclnbgr6  48661  dfsclnbgr6  48663  uhgrimedg  48696  uhgrimprop  48697  isuspgrimlem  48700  isuspgrim  48701  gricushgr  48722  uhgrimisgrgric  48736  isubgr3stgrlem7  48777  uspgrlimlem2  48794  gpgedgel  48855  gpgprismgriedgdmss  48857  gpgedgvtx0  48866  gpgedgiov  48870  gpgedg2ov  48871  gpgedg2iv  48872  gpg5nbgrvtx03starlem2  48874  gpg5nbgrvtx13starlem1  48876  gpg5nbgrvtx13starlem3  48878  gpg5nbgrvtx03star  48885  gpg5nbgr3star  48886  gpg5gricstgr3  48895  pgnbgreunbgrlem4  48924  assintop  49014  uzlidlring  49040  2zrngnmrid  49061  cznrng  49066  lmodvsmdi  49199  lincsum  49249  lincsumcl  49251  el0ldep  49286  ldepspr  49293  lindssnlvec  49306  nn0digval  49420  1arympt1fv  49459  eenglngeehlnmlem1  49557  rrx2linest  49562  line2  49572  itsclc0yqe  49581  r19.41dv  49620  setrec1lem3  50507  aacllem  50661