Theorem anim1i 616

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  sylanl1  678  sylanr1  680  eu6im  2659  r19.28v  3189  rmob  3877  eqeuel  4325  preq12nebg  4796  fores  6603  ssimaex  6751  dffv2  6759  exfo  6874  fpropnf1  7028  oprabv  7217  ndmovass  7339  fun11uni  7640  fabexg  7642  f1oabexg  7645  f1iun  7648  soxp  7826  tz7.48lem  8080  tz7.49c  8085  omass  8209  oewordri  8221  omabs  8277  sbthlem9  8638  fineqvlem  8735  pssnn  8739  domunfican  8794  fiint  8798  fsuppsssupp  8852  sup0  8933  inf1  9088  infeq5  9103  cantnfle  9137  rankuni  9295  djuunxp  9353  acndom  9480  acnnum  9481  cdainflem  9616  cfcof  9699  ac6num  9904  ac6s2  9911  brdom5  9954  brdom4  9955  genpnnp  10430  divmulasscom  11325  lediv2a  11537  supmul1  11613  infregelb  11628  nn2ge  11667  btwnz  12087  eluz2b2  12324  uz2mulcl  12329  eqreznegel  12337  xrsupexmnf  12701  xrinfmexpnf  12702  xrsupsslem  12703  xrinfmsslem  12704  supxrun  12712  ioo0  12766  elioo4g  12800  fz0fzelfz0  13016  fz0fzdiffz0  13019  2ffzeq  13031  elfzodifsumelfzo  13106  elfzom1elp1fzo  13107  zpnn0elfzo  13113  elfzom1elp1fzo1  13140  fzonfzoufzol  13143  quoremnn0  13227  zmodidfzoimp  13272  modabs  13275  modmuladd  13284  modifeq2int  13304  modaddmulmod  13309  expcl2lem  13444  hashgt23el  13788  hashreshashfun  13803  iswrdsymb  13884  ccatcl  13929  ccatsymb  13939  swrdfv2  14026  swrdsbslen  14029  swrdspsleq  14030  pfxswrd  14071  pfxccatin12lem3  14097  pfxccatpfx2  14102  swrdccat3blem  14104  reuccatpfxs1  14112  repswccat  14151  cshweqdifid  14185  lswco  14204  repsco  14205  s4f1o  14283  ccat2s1fvwALTOLD  14322  trclun  14377  mulre  14483  rediv  14493  imdiv  14500  resqrex  14613  caurcvg2  15037  fsumdifsnconst  15149  modfsummods  15151  tanval  15484  p1modz1  15617  negdvdsb  15629  muldvds1  15637  muldvds2  15638  dvdscmulr  15641  dvdsmulcr  15642  sumodd  15742  divalglem8  15754  divgcdnn  15866  lcmfunsnlem2lem2  15986  lcmfun  15992  2mulprm  16040  maxprmfct  16056  vfermltlALT  16142  modprm0  16145  pcpremul  16183  pcmul  16191  oddprmdvds  16242  prmdvdsprmo  16381  cshwsidrepsw  16430  gsumccat  18009  grpissubg  18302  gsmsymgreqlem2  18562  symgfixfo  18570  fsfnn0gsumfsffz  19106  irredn0  19456  gim0to0  19498  rim0to0OLD  19499  lsppratlem1  19922  dvdsrzring  20633  mpofrlmd  20924  matinvgcell  21047  mat1dimcrng  21089  dmatscmcl  21115  scmatscm  21125  scmatghm  21145  scmatmhm  21146  ma1repvcl  21182  slesolinv  21292  slesolinvbi  21293  cramerimplem1  21295  cramerimp  21298  cramerlem1  21299  cramer  21303  cpmatacl  21327  cpmatmcl  21330  mat2pmatghm  21341  mat2pmatmul  21342  m2pmfzgsumcl  21359  decpmatmul  21383  decpmatmulsumfsupp  21384  pmatcollpwfi  21393  pm2mpf1  21410  pm2mpghm  21427  pm2mpmhmlem1  21429  monmat2matmon  21435  chpdmatlem2  21450  chpdmat  21452  cpmadugsumlemB  21485  cpmadugsumlemC  21486  cpmadugsumlemF  21487  clscld  21658  neiptopnei  21743  2ndcdisj2  22068  comppfsc  22143  tx1stc  22261  opnfbas  22453  fbasfip  22479  alexsublem  22655  alexsubALTlem4  22661  cnextcn  22678  ngpocelbl  23316  cphipval  23849  bcthlem5  23934  vitalilem4  24215  vitalilem5  24216  itg2mulc  24351  dvcobr  24546  dvcnvlem  24576  dvferm1  24585  dvne0  24611  mdegmullem  24675  plyeq0lem  24803  plyexmo  24905  aalioulem5  24928  aalioulem6  24929  aaliou  24930  cxple2a  25285  cxpaddlelem  25335  cxpaddle  25336  relogbcxpb  25368  bcmono  25856  lgsprme0  25918  gausslemma2dlem0e  25939  gausslemma2dlem1a  25944  gausslemma2dlem6  25951  lgsquadlem2  25960  2lgsoddprm  25995  colinearalg  26699  axcontlem3  26755  umgrislfupgrlem  26910  edgupgr  26922  usgruspgrb  26969  usgrislfuspgr  26972  edgssv2  26983  umgr2edg  26994  uspgredg2v  27009  usgrexmplef  27044  subupgr  27072  subusgr  27074  nbupgrres  27149  nb3gr2nb  27169  nbupgruvtxres  27192  cusgrres  27233  cusgrsizeindslem  27236  cusgrsizeinds  27237  vtxdun  27266  finrusgrfusgr  27350  cusgrrusgr  27366  spthdep  27518  cycliscrct  27583  crctcshwlkn0lem6  27596  crctcshwlkn0lem7  27597  crctcshtrl  27604  crctcsh  27605  umgr2adedgwlkonALT  27729  elwwlks2  27748  elwspths2spth  27749  rusgrnumwwlk  27757  clwlkclwwlklem2a  27779  clwlkclwwlklem3  27782  clwwisshclwws  27796  wwlksubclwwlk  27840  eleclclwwlknlem2  27843  eupth2lem3lem3  28012  eucrct2eupth1  28026  frgr3v  28057  3vfriswmgr  28060  1to3vfriswmgr  28062  3cyclfrgr  28070  vdgn1frgrv2  28078  frgrwopreglem5  28103  frgrwopreglem5ALT  28104  frrusgrord0lem  28121  frrusgrord0  28122  2clwwlk2clwwlk  28132  extwwlkfab  28134  numclwwlk1lem2fo  28140  friendshipgt3  28180  ex-natded9.20-2  28200  grpoidinvlem3  28286  grpoidinv  28288  nmobndseqi  28559  nmobndseqiALT  28560  hvaddsub4  28858  ocsh  29063  5oalem2  29435  5oalem5  29438  3oalem2  29443  pjjsi  29480  hoadddir  29584  leopmul  29914  stge1i  30018  hatomistici  30142  mdsymlem2  30184  mdsymlem5  30187  addltmulALT  30226  isoun  30440  fsumiunle  30549  lsmsnorb  30949  crefdf  31116  qqhre  31265  esumiun  31357  sxbrsigalem0  31533  dya2iocnei  31544  sxbrsigalem5  31550  sibfinima  31601  eulerpartlemgs2  31642  ballotlemfc0  31754  ballotlemfcc  31755  ballotlemsup  31766  bnj529  32016  bnj945  32049  bnj1098  32059  bnj1533  32128  bnj605  32183  bnj594  32188  bnj607  32192  bnj966  32220  bnj967  32221  bnj996  32232  bnj999  32234  bnj1006  32236  bnj1118  32260  bnj1172  32277  bnj1279  32294  bnj1296  32297  bnj1498  32337  lfuhgr3  32370  loop1cycl  32388  cvmsi  32516  satf0op  32628  satffunlem1lem1  32653  satffunlem2lem1  32655  fv2ndcnv  33025  elno2  33165  trisegint  33493  funtransport  33496  btwnconn1lem4  33555  btwnconn2  33567  segcon2  33570  outsideofeu  33596  isfne  33691  lukshef-ax2  33767  limsucncmpi  33797  bj-nsnid  34366  bj-restn0b  34386  bj-eldiag2  34473  bj-isrvec2  34585  pibt2  34702  unccur  34879  lindsadd  34889  lindsenlbs  34891  matunitlindflem1  34892  matunitlindflem2  34893  poimirlem26  34922  poimirlem27  34923  poimirlem29  34925  poimirlem30  34926  poimirlem32  34928  heicant  34931  ismblfin  34937  itg2gt0cn  34951  bddiblnc  34966  areacirc  34991  opelopab3  34996  isdivrngo  35232  isdrngo2  35240  fldcrng  35286  flddmn  35340  refrelredund4  35874  cmtbr4N  36395  linepsubN  36892  pmapsub  36908  paddasslem14  36973  pclcmpatN  37041  trlval2  37303  cdleme20  37464  cdleme21j  37476  dvalveclem  38165  dia2dimlem7  38210  dvhlveclem  38248  docaclN  38264  dihjat1  38569  mapdhcl  38867  mapdh6dN  38879  mapdh8  38928  hdmap1l6d  38953  hdmap10  38980  hdmaprnlem17N  39003  hdmaplkr  39053  hdmapip0  39055  hgmapvv  39066  cmpfiiin  39300  pellexlem4  39435  pellqrex  39482  acongtr  39581  acongrep  39583  jm2.23  39599  rp-fakeanorass  39885  rp-isfinite6  39890  harval3  39910  inintabss  39944  rfovcnvf1od  40356  clsk1indlem3  40399  ntrclsk13  40427  pm10.55  40707  refsum2cnlem1  41300  axccd2  41502  mptssid  41517  fmuldfeq  41870  climsuse  41895  limclner  41938  climxlim2lem  42132  icccncfext  42176  stoweidlem26  42318  stoweidlem52  42344  stoweidlem57  42349  fourierdlem20  42419  fourierdlem41  42440  fourierdlem52  42450  fourierdlem64  42462  fourierdlem102  42500  fourierdlem114  42512  ovolval4lem1  42938  preimagelt  42987  preimalegt  42988  funressneu  43289  afvelrn  43374  elfz2z  43522  2ffzoeq  43535  imasetpreimafvbijlemfv  43569  imasetpreimafvbijlemf1  43571  fargshiftfva  43610  ichreuopeq  43642  2exopprim  43694  reuopreuprim  43695  fmtnoprmfac1  43734  proththd  43786  opoeALTV  43855  evensumeven  43879  sbgoldbalt  43953  evengpop3  43970  evengpoap3  43971  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  wtgoldbnnsum4prm  43974  bgoldbnnsum3prm  43976  tgoldbach  43989  isomushgr  43998  uspgrsprfo  44030  assintop  44123  isringrng  44159  rnglz  44162  c0snmgmhm  44192  zrrnghm  44195  uzlidlring  44207  2zrngnmrid  44228  cznrng  44233  rnghmsubcsetclem2  44254  rhmsubcsetclem2  44300  rhmsubcrngclem2  44306  lmodvsmdi  44437  lincsum  44491  lincsumcl  44493  el0ldep  44528  ldepspr  44535  lindssnlvec  44548  modn0mul  44587  m1modmmod  44588  nn0digval  44667  eenglngeehlnmlem1  44731  rrx2linest  44736  line2  44746  itsclc0yqe  44755  setrec1lem3  44799  aacllem  44909