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 395

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 207  df-an 396

This theorem is referenced by:  sylanl1  681  sylanr1  683  eu6im  2576  r19.28v  3169  rmob  3842  eqeuel  4319  preq12nebg  4821  fores  6764  fdmeu  6898  ssimaex  6927  dffv2  6937  exfo  7059  fpropnf1  7223  f1ocoima  7259  oprabv  7428  ndmovass  7556  fun11uni  7885  resf1ext2b  7887  fabexgOLD  7891  f1oabexgOLD  7895  f1iun  7898  soxp  8081  tz7.48lem  8382  tz7.49c  8387  omass  8517  oewordri  8530  omabs  8589  sbthlem9  9035  pssnn  9105  fineqvlem  9178  domunfican  9234  fiint  9239  fsuppsssupp  9296  sup0  9382  inf1  9543  infeq5  9558  cantnfle  9592  rankuni  9787  djuunxp  9845  acndom  9973  acnnum  9974  cdainflem  10110  cfcof  10196  ac6num  10401  ac6s2  10408  brdom5  10451  brdom4  10452  genpnnp  10928  divmulasscom  11832  lediv2a  12048  supmul1  12123  infregelb  12138  nn2ge  12184  btwnz  12607  eluz2b2  12846  uz2mulcl  12851  eqreznegel  12859  xrsupexmnf  13232  xrinfmexpnf  13233  xrsupsslem  13234  xrinfmsslem  13235  supxrun  13243  ioo0  13298  elioo4g  13334  fz0fzelfz0  13562  fz0fzdiffz0  13565  2ffzeq  13577  elfzodifsumelfzo  13659  elfzom1elp1fzo  13660  zpnn0elfzo  13666  elfzom1elp1fzo1  13695  fzonfzoufzol  13699  quoremnn0  13788  zmodidfzoimp  13833  modabs  13836  modaddb  13841  modifeq2int  13868  modaddmulmod  13873  expcl2lem  14008  hashgt23el  14359  hashreshashfun  14374  iswrdsymb  14466  ccatcl  14509  ccatsymb  14518  swrdfv2  14597  swrdsbslen  14600  swrdspsleq  14601  pfxswrd  14641  pfxccatin12lem3  14667  pfxccatpfx2  14672  swrdccat3blem  14674  reuccatpfxs1  14682  repswccat  14721  cshweqdifid  14755  lswco  14774  repsco  14775  s4f1o  14853  trclun  14949  mulre  15056  rediv  15066  imdiv  15073  resqrex  15185  caurcvg2  15613  fsumdifsnconst  15726  modfsummods  15728  tanval  16065  p1modz1  16198  negdvdsb  16211  muldvds1  16219  muldvds2  16220  dvdscmulr  16223  dvdsmulcr  16224  sumodd  16327  divalglem8  16339  divgcdnn  16454  lcmfunsnlem2lem2  16578  lcmfun  16584  2mulprm  16632  maxprmfct  16648  vfermltlALT  16742  modprm0  16745  pcpremul  16783  pcmul  16791  oddprmdvds  16843  prmdvdsprmo  16982  cshwsidrepsw  17033  gsumccat  18778  grpissubg  19088  ecqusaddd  19133  ecqusaddcl  19134  eqg0subg  19137  gim0to0  19210  gsmsymgreqlem2  19372  symgfixfo  19380  fsfnn0gsumfsffz  19924  rnglz  20112  isringrng  20234  irredn0  20371  c0snmgmhm  20410  rimisrngim  20443  zrrnghm  20481  rnghmsubcsetclem2  20577  rhmsubcsetclem2  20606  rhmsubcrngclem2  20612  lsppratlem1  21114  qusmulrng  21249  quscrng  21250  rngqiprngghmlem3  21256  rngqiprnglinlem3  21260  rngqiprngimf1lem  21261  rngqiprnglin  21269  cnfldfunALT  21336  cnfldfunALTOLD  21349  dvdsrzring  21428  mpofrlmd  21744  matinvgcell  22391  mat1dimcrng  22433  dmatscmcl  22459  scmatscm  22469  scmatghm  22489  scmatmhm  22490  ma1repvcl  22526  slesolinv  22636  slesolinvbi  22637  cramerimplem1  22639  cramerimp  22642  cramerlem1  22643  cramer  22647  cpmatacl  22672  cpmatmcl  22675  mat2pmatghm  22686  mat2pmatmul  22687  m2pmfzgsumcl  22704  decpmatmul  22728  decpmatmulsumfsupp  22729  pmatcollpwfi  22738  pm2mpf1  22755  pm2mpghm  22772  pm2mpmhmlem1  22774  monmat2matmon  22780  chpdmatlem2  22795  chpdmat  22797  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  clscld  23003  neiptopnei  23088  2ndcdisj2  23413  comppfsc  23488  tx1stc  23606  opnfbas  23798  fbasfip  23824  alexsublem  24000  alexsubALTlem4  24006  cnextcn  24023  ngpocelbl  24660  cphipval  25211  bcthlem5  25296  vitalilem4  25580  vitalilem5  25581  itg2mulc  25716  bddiblnc  25811  dvcobr  25917  dvcobrOLD  25918  dvcnvlem  25948  dvferm1  25957  dvne0  25984  mdegmullem  26051  plyeq0lem  26183  plyexmo  26289  aalioulem5  26312  aalioulem6  26313  aaliou  26314  cxple2a  26676  cxpaddlelem  26729  cxpaddle  26730  relogbcxpb  26765  bcmono  27256  lgsprme0  27318  gausslemma2dlem0e  27339  gausslemma2dlem1a  27344  gausslemma2dlem6  27351  lgsquadlem2  27360  2lgsoddprm  27395  elno2  27634  cofcutr  27932  colinearalg  28995  axcontlem3  29051  umgrislfupgrlem  29207  edgupgr  29219  usgruspgrb  29268  usgrislfuspgr  29272  edgssv2  29283  umgr2edg  29294  uspgredg2v  29309  usgrexmplef  29344  subupgr  29372  subusgr  29374  nbupgrres  29449  nb3gr2nb  29469  nbupgruvtxres  29492  cusgrres  29534  cusgrsizeindslem  29537  cusgrsizeinds  29538  vtxdun  29567  finrusgrfusgr  29651  cusgrrusgr  29667  pthdifv  29815  spthdep  29819  cycliscrct  29884  crctcshwlkn0lem6  29900  crctcshwlkn0lem7  29901  crctcshtrl  29908  crctcsh  29909  umgr2adedgwlkonALT  30032  elwwlks2  30054  elwspths2spth  30055  rusgrnumwwlk  30063  clwlkclwwlklem2a  30085  clwlkclwwlklem3  30088  clwwisshclwws  30102  wwlksubclwwlk  30145  eleclclwwlknlem2  30148  eupth2lem3lem3  30317  eucrct2eupth1  30331  frgr3v  30362  3vfriswmgr  30365  1to3vfriswmgr  30367  3cyclfrgr  30375  vdgn1frgrv2  30383  frgrwopreglem5  30408  frgrwopreglem5ALT  30409  frrusgrord0lem  30426  frrusgrord0  30427  2clwwlk2clwwlk  30437  extwwlkfab  30439  numclwwlk1lem2fo  30445  friendshipgt3  30485  ex-natded9.20-2  30505  grpoidinvlem3  30593  grpoidinv  30595  nmobndseqi  30866  nmobndseqiALT  30867  hvaddsub4  31165  ocsh  31370  5oalem2  31742  5oalem5  31745  3oalem2  31750  pjjsi  31787  hoadddir  31891  leopmul  32221  stge1i  32325  hatomistici  32449  mdsymlem2  32491  mdsymlem5  32494  addltmulALT  32533  isoun  32791  fsumiunle  32920  lsmsnorb  33483  crefdf  34025  qqhre  34197  esumiun  34271  sxbrsigalem0  34448  dya2iocnei  34459  sxbrsigalem5  34465  sibfinima  34516  eulerpartlemgs2  34557  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemsup  34682  bnj529  34917  bnj945  34949  bnj1098  34959  bnj1533  35027  bnj605  35082  bnj594  35087  bnj607  35091  bnj966  35119  bnj967  35120  bnj996  35131  bnj999  35133  bnj1006  35135  bnj1118  35159  bnj1172  35176  bnj1279  35193  bnj1296  35196  bnj1498  35236  fnrelpredd  35266  lfuhgr3  35333  loop1cycl  35350  cvmsi  35478  satf0op  35590  satffunlem1lem1  35615  satffunlem2lem1  35617  fv2ndcnv  35991  trisegint  36241  funtransport  36244  btwnconn1lem4  36303  btwnconn2  36315  segcon2  36318  outsideofeu  36344  isfne  36552  lukshef-ax2  36628  limsucncmpi  36658  weiunso  36679  bj-nsnid  37312  bj-restn0b  37338  bj-eldiag2  37426  bj-isrvec2  37549  pibt2  37666  unccur  37848  lindsadd  37858  lindsenlbs  37860  matunitlindflem1  37861  matunitlindflem2  37862  poimirlem26  37891  poimirlem27  37892  poimirlem29  37894  poimirlem30  37895  poimirlem32  37897  heicant  37900  ismblfin  37906  itg2gt0cn  37920  areacirc  37958  opelopab3  37963  isdivrngo  38195  isdrngo2  38203  fldcrngo  38249  flddmn  38303  refrelredund4  38964  mainer2  39205  cmtbr4N  39625  linepsubN  40122  pmapsub  40138  paddasslem14  40203  pclcmpatN  40271  trlval2  40533  cdleme20  40694  cdleme21j  40706  dvalveclem  41395  dia2dimlem7  41440  dvhlveclem  41478  docaclN  41494  dihjat1  41799  mapdhcl  42097  mapdh6dN  42109  mapdh8  42158  hdmap1l6d  42183  hdmap10  42210  hdmaprnlem17N  42233  hdmaplkr  42283  hdmapip0  42285  hgmapvv  42296  aks6d1c4  42488  cmpfiiin  43048  pellexlem4  43183  pellqrex  43230  acongtr  43329  acongrep  43331  jm2.23  43347  omlimcl2  43593  onsucf1lem  43620  oege1  43657  nnoeomeqom  43663  cantnfresb  43675  onmcl  43682  tfsconcat0i  43696  ofoafg  43705  ofoafo  43707  ofoaass  43711  ofoacom  43712  naddcnfass  43720  rp-fakeanorass  43863  rp-isfinite6  43868  harval3  43888  inintabss  43928  rfovcnvf1od  44354  clsk1indlem3  44393  ntrclsk13  44421  pm10.55  44719  refsum2cnlem1  45391  axccd2  45582  mptssid  45593  fmuldfeq  45937  climsuse  45962  limclner  46003  climxlim2lem  46197  icccncfext  46239  stoweidlem26  46378  stoweidlem52  46404  stoweidlem57  46409  fourierdlem20  46479  fourierdlem41  46500  fourierdlem52  46510  fourierdlem64  46522  fourierdlem102  46560  fourierdlem114  46572  ovolval4lem1  47001  preimagelt  47051  preimalegt  47052  squeezedltsq  47240  funressneu  47401  afvelrn  47522  elfz2z  47669  2ffzoeq  47681  zplusmodne  47697  addmodne  47698  minusmod5ne  47703  modn0mul  47711  m1modmmod  47712  imasetpreimafvbijlemfv  47756  imasetpreimafvbijlemf1  47758  fargshiftfva  47797  ichreuopeq  47827  2exopprim  47879  reuopreuprim  47880  fmtnoprmfac1  47919  proththd  47968  opoeALTV  48037  evensumeven  48061  sbgoldbalt  48135  evengpop3  48152  evengpoap3  48153  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  wtgoldbnnsum4prm  48156  bgoldbnnsum3prm  48158  tgoldbach  48171  dfclnbgr6  48210  dfsclnbgr6  48212  uhgrimedg  48245  uhgrimprop  48246  isuspgrimlem  48249  isuspgrim  48250  gricushgr  48271  uhgrimisgrgric  48285  isubgr3stgrlem7  48326  uspgrlimlem2  48343  gpgedgel  48404  gpgprismgriedgdmss  48406  gpgedgvtx0  48415  gpgedgiov  48419  gpgedg2ov  48420  gpgedg2iv  48421  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem3  48427  gpg5nbgrvtx03star  48434  gpg5nbgr3star  48435  gpg5gricstgr3  48444  pgnbgreunbgrlem4  48473  assintop  48563  uzlidlring  48589  2zrngnmrid  48610  cznrng  48615  lmodvsmdi  48733  lincsum  48783  lincsumcl  48785  el0ldep  48820  ldepspr  48827  lindssnlvec  48840  nn0digval  48954  1arympt1fv  48993  eenglngeehlnmlem1  49091  rrx2linest  49096  line2  49106  itsclc0yqe  49115  r19.41dv  49155  setrec1lem3  50042  aacllem  50154