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  ax12ev2c  2220  eu6im  2603  r19.28v  3197  rmob  3841  eqeuel  4316  preq12nebg  4821  fores  6828  fdmeu  6964  ssimaex  6993  dffv2  7003  exfo  7129  fpropnf1  7294  f1ocoima  7334  oprabv  7503  ndmovass  7633  fun11uni  7969  resf1ext2b  7971  f1iun  7980  soxp  8168  tz7.48lemOLD  8479  tz7.49c  8484  omass  8616  oewordri  8629  omabs  8688  sbthlem9  9142  pssnn  9212  fineqvlem  9285  domunfican  9341  fiint  9346  fsuppsssupp  9400  sup0  9486  inf1  9650  infeq5  9665  cantnfle  9699  rankuni  9906  setrec1lem3  9996  djuunxp  10029  acndom  10157  acnnum  10158  cdainflem  10293  cfcof  10379  ac6num  10584  ac6s2  10591  brdom5  10635  brdom4  10636  genpnnp  11117  divmulasscom  12025  lediv2a  12238  supmul1  12313  infregelb  12328  nn2ge  12392  btwnz  12829  eluz2b2  13075  uz2mulcl  13080  eqreznegel  13088  xrsupexmnf  13462  xrinfmexpnf  13463  xrsupsslem  13464  xrinfmsslem  13465  supxrun  13473  ioo0  13528  elioo4g  13564  fz0fzelfz0  13795  fz0fzdiffz0  13798  2ffzeq  13810  elfzodifsumelfzo  13893  elfzom1elp1fzo  13894  zpnn0elfzo  13900  elfzom1elp1fzo1  13929  fzonfzoufzol  13933  quoremnn0  14023  zmodidfzoimp  14068  modabs  14071  modaddb  14076  modifeq2int  14103  modaddmulmod  14108  expcl2lem  14243  hashgt23el  14596  hashreshashfun  14611  iswrdsymb  14703  ccatcl  14746  ccatsymb  14755  swrdfv2  14839  swrdsbslen  14842  swrdspsleq  14843  pfxswrd  14883  pfxccatin12lem3  14909  pfxccatpfx2  14914  swrdccat3blem  14916  reuccatpfxs1  14924  repswccat  14965  cshweqdifid  14999  lswco  15018  repsco  15019  s4f1o  15098  trclun  15196  mulre  15317  rediv  15327  imdiv  15334  resqrex  15446  caurcvg2  15874  fsumdifsnconst  15987  modfsummods  15989  tanval  16325  p1modz1  16458  negdvdsb  16471  muldvds1  16479  muldvds2  16480  dvdscmulr  16483  dvdsmulcr  16484  sumodd  16587  divalglem8  16599  divgcdnn  16716  lcmfunsnlem2lem2  16843  lcmfun  16849  2mulprm  16897  maxprmfct  16914  vfermltlALT  17009  modprm0  17012  pcpremul  17050  pcmul  17058  oddprmdvds  17110  prmdvdsprmo  17249  cshwsidrepsw  17300  gsumccat  19066  grpissubg  19386  ecqusaddd  19436  ecqusaddcl  19437  eqg0subg  19440  gim0to0  19512  gsmsymgreqlem2  19675  symgfixfo  19683  fsfnn0gsumfsffz  20227  rnglz  20417  isringrng  20546  irredn0  20683  c0snmgmhm  20722  rimisrngim  20765  zrrnghm  20818  rnghmsubcsetclem2  20914  rhmsubcsetclem2  20943  rhmsubcrngclem2  20949  lsppratlem1  21455  qusmulrng  21608  quscrng  21609  rngqiprngghmlem3  21615  rngqiprnglinlem3  21619  rngqiprngimf1lem  21620  rngqiprnglin  21628  cnfldfunALT  21723  dvdsrzring  21797  mpofrlmd  22113  lindsenlbs  22187  matinvgcell  22780  mat1dimcrng  22822  dmatscmcl  22848  scmatscm  22858  scmatghm  22878  scmatmhm  22879  ma1repvcl  22915  matunitlindflem1  23024  matunitlindflem2  23025  slesolinv  23028  slesolinvbi  23029  cramerimplem1  23031  cramerimp  23034  cramerlem1  23035  cramer  23039  cpmatacl  23064  cpmatmcl  23067  mat2pmatghm  23078  mat2pmatmul  23079  m2pmfzgsumcl  23096  decpmatmul  23120  decpmatmulsumfsupp  23121  pmatcollpwfi  23130  pm2mpf1  23147  pm2mpghm  23164  pm2mpmhmlem1  23166  monmat2matmon  23172  chpdmatlem2  23187  chpdmat  23189  cpmadugsumlemB  23222  cpmadugsumlemC  23223  cpmadugsumlemF  23224  clscld  23395  neiptopnei  23480  2ndcdisj2  23806  comppfsc  23881  tx1stc  23999  opnfbas  24191  fbasfip  24217  alexsublem  24393  alexsubALTlem4  24399  cnextcn  24416  ngpocelbl  25053  cphipval  25594  bcthlem5  25679  vitalilem4  25962  vitalilem5  25963  itg2mulc  26098  bddiblnc  26192  dvcobr  26296  dvcnvlem  26326  dvferm1  26335  dvne0  26361  mdegmullem  26426  plyeq0lem  26559  plyexmo  26666  aalioulem5  26693  aalioulem6  26694  aaliou  26695  cxple2a  27057  cxpaddlelem  27109  cxpaddle  27110  relogbcxpb  27145  bcmono  27634  lgsprme0  27696  gausslemma2dlem0e  27717  gausslemma2dlem1a  27722  gausslemma2dlem6  27729  lgsquadlem2  27738  2lgsoddprm  27773  flt4lem2  28007  fltoprmlem1  28023  elno2  28041  cofcutr  28340  colinearalg  29518  axcontlem3  29574  umgrislfupgrlem  29730  edgupgr  29742  lfuhgr3  29758  usgruspgrb  29794  usgrislfuspgr  29798  edgssv2  29809  umgr2edg  29820  uspgredg2v  29835  usgrexmplef  29870  subupgr  29898  subusgr  29900  nbupgrres  29975  nb3gr2nb  29995  nbupgruvtxres  30018  cusgrres  30059  cusgrsizeindslem  30062  cusgrsizeinds  30063  vtxdun  30092  finrusgrfusgr  30176  cusgrrusgr  30192  pthdifv  30346  spthdep  30350  cycliscrct  30417  crctcshwlkn0lem6  30434  crctcshwlkn0lem7  30435  crctcshtrl  30442  crctcsh  30443  umgr2adedgwlkonALT  30566  elwwlks2  30588  elwspths2spth  30589  rusgrnumwwlk  30597  clwlkclwwlklem2a  30619  clwlkclwwlklem3  30622  clwwisshclwws  30636  wwlksubclwwlk  30679  eleclclwwlknlem2  30682  loop1cycl  30774  eupth2lem3lem3  30861  eucrct2eupth1  30875  frgr3v  30906  3vfriswmgr  30909  1to3vfriswmgr  30911  3cyclfrgr  30919  vdgn1frgrv2  30927  frgrwopreglem5  30952  frgrwopreglem5ALT  30953  frrusgrord0lem  30970  frrusgrord0  30971  2clwwlk2clwwlk  30981  extwwlkfab  30983  numclwwlk1lem2fo  30989  friendshipgt3  31029  ex-natded9.20-2  31049  grpoidinvlem3  31138  grpoidinv  31140  nmobndseqi  31411  nmobndseqiALT  31412  hvaddsub4  31710  ocsh  31915  5oalem2  32287  5oalem5  32290  3oalem2  32295  pjjsi  32332  hoadddir  32436  leopmul  32766  stge1i  32870  hatomistici  32994  mdsymlem2  33036  mdsymlem5  33039  addltmulALT  33120  isoun  33366  fsumiunle  33490  lsmsnorb  34016  crefdf  34550  qqhre  34722  esumiun  34796  sxbrsigalem0  34973  dya2iocnei  34984  sxbrsigalem5  34990  sibfinima  35041  eulerpartlemgs2  35082  ballotlemfc0  35195  ballotlemfcc  35196  ballotlemsup  35207  bnj529  35442  bnj945  35474  bnj1098  35484  bnj1533  35552  bnj605  35607  bnj594  35612  bnj607  35616  bnj966  35644  bnj967  35645  bnj996  35656  bnj999  35658  bnj1006  35660  bnj1118  35684  bnj1172  35701  bnj1279  35718  bnj1296  35721  bnj1498  35761  fnrelpredd  35804  ptpconn  36165  cvmsi  36197  satf0op  36309  satffunlem1lem1  36334  satffunlem2lem1  36336  mirimanofffr  36629  fv2ndcnv  36720  trisegint  36971  funtransport  36974  btwnconn1lem4  37033  btwnconn2  37045  segcon2  37048  outsideofeu  37074  isfne  37305  lukshef-ax2  37381  limsucncmpi  37411  weiunso  37432  bj-nsnid  38176  bj-restn0b  38203  bj-eldiag2  38290  bj-isrvec2  38413  pibt2  38532  unccur  38718  lindsadd  38728  poimirlem26  38756  poimirlem27  38757  poimirlem29  38759  poimirlem30  38760  poimirlem32  38762  heicant  38765  ismblfin  38771  itg2gt0cn  38785  areacirc  38823  impprop  38836  opelopab3  38844  isdivrngo  39076  isdrngo2  39084  fldcrngo  39130  flddmn  39184  refrelredund4  39843  mainer2  40084  cmtbr4N  40504  linepsubN  41001  pmapsub  41017  paddasslem14  41082  pclcmpatN  41150  trlval2  41412  cdleme20  41573  cdleme21j  41585  dvalveclem  42274  dia2dimlem7  42319  dvhlveclem  42357  docaclN  42373  dihjat1  42678  mapdhcl  42976  mapdh6dN  42988  mapdh8  43037  hdmap1l6d  43062  hdmap10  43089  hdmaprnlem17N  43112  hdmaplkr  43162  hdmapip0  43164  hgmapvv  43175  aks6d1c4  43366  cmpfiiin  43901  pellexlem4  44032  pellqrex  44079  acongtr  44178  acongrep  44180  jm2.23  44196  omlimcl2  44436  onsucf1lem  44463  oege1  44500  nnoeomeqom  44506  cantnfresb  44518  onmcl  44525  tfsconcat0i  44539  ofoafg  44548  ofoafo  44550  ofoaass  44554  ofoacom  44555  naddcnfass  44563  rp-fakeanorass  44706  rp-isfinite6  44711  harval3  44731  inintabss  44771  rfovcnvf1od  45196  clsk1indlem3  45235  ntrclsk13  45263  pm10.55  45545  refsum2cnlem1  46259  axccd2  46447  mptssid  46458  fmuldfeq  46800  climsuse  46825  limclner  46866  climxlim2lem  47060  icccncfext  47102  stoweidlem26  47241  stoweidlem52  47267  stoweidlem57  47272  fourierdlem20  47342  fourierdlem41  47363  fourierdlem52  47373  fourierdlem64  47385  fourierdlem102  47423  fourierdlem114  47435  ovolval4lem1  47864  preimagelt  47914  preimalegt  47915  squeezedltsq  48117  funressneu  48322  afvelrn  48443  elfz2z  48590  2ffzoeq  48603  zplusmodne  48624  addmodne  48625  minusmod5ne  48630  modn0mul  48638  m1modmmod  48639  nndivides2  48659  imasetpreimafvbijlemfv  48689  imasetpreimafvbijlemf1  48691  fargshiftfva  48730  ichreuopeq  48760  2exopprim  48812  reuopreuprim  48813  fmtnoprmfac1  48855  proththd  48904  opoeALTV  48986  evensumeven  49010  sbgoldbalt  49084  evengpop3  49101  evengpoap3  49102  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  wtgoldbnnsum4prm  49105  bgoldbnnsum3prm  49107  tgoldbach  49120  dfclnbgr6  49159  dfsclnbgr6  49161  uhgrimedg  49194  uhgrimprop  49195  isuspgrimlem  49198  isuspgrim  49199  gricushgr  49220  uhgrimisgrgric  49234  isubgr3stgrlem7  49275  uspgrlimlem2  49292  gpgedgel  49353  gpgprismgriedgdmss  49355  gpgedgvtx0  49364  gpgedgiov  49368  gpgedg2ov  49369  gpgedg2iv  49370  gpg5nbgrvtx03starlem2  49372  gpg5nbgrvtx13starlem1  49374  gpg5nbgrvtx13starlem3  49376  gpg5nbgrvtx03star  49383  gpg5nbgr3star  49384  gpg5gricstgr3  49393  pgnbgreunbgrlem4  49422  assintop  49511  uzlidlring  49537  2zrngnmrid  49558  cznrng  49563  lmodvsmdi  49696  lincsum  49746  lincsumcl  49748  el0ldep  49783  ldepspr  49790  lindssnlvec  49803  nn0digval  49917  1arympt1fv  49956  eenglngeehlnmlem1  50055  rrx2linest  50059  line2  50069  itsclc0yqe  50078  r19.41dv  50117  aacllem  51219