Theorem anim1i 615

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 613	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  680  sylanr1  682  eu6im  2575  r19.28v  3190  rmob  3890  eqeuel  4365  preq12nebg  4863  fores  6830  fdmeu  6965  ssimaex  6994  dffv2  7004  exfo  7125  fpropnf1  7287  f1ocoima  7323  oprabv  7493  ndmovass  7621  fun11uni  7955  resf1ext2b  7957  fabexgOLD  7961  f1oabexgOLD  7965  f1iun  7968  soxp  8154  tz7.48lem  8481  tz7.49c  8486  omass  8618  oewordri  8630  omabs  8689  sbthlem9  9131  pssnn  9208  fineqvlem  9298  domunfican  9361  fiint  9366  fiintOLD  9367  fsuppsssupp  9421  sup0  9506  inf1  9662  infeq5  9677  cantnfle  9711  rankuni  9903  djuunxp  9961  acndom  10091  acnnum  10092  cdainflem  10228  cfcof  10314  ac6num  10519  ac6s2  10526  brdom5  10569  brdom4  10570  genpnnp  11045  divmulasscom  11946  lediv2a  12162  supmul1  12237  infregelb  12252  nn2ge  12293  btwnz  12721  eluz2b2  12963  uz2mulcl  12968  eqreznegel  12976  xrsupexmnf  13347  xrinfmexpnf  13348  xrsupsslem  13349  xrinfmsslem  13350  supxrun  13358  ioo0  13412  elioo4g  13447  fz0fzelfz0  13674  fz0fzdiffz0  13677  2ffzeq  13689  elfzodifsumelfzo  13770  elfzom1elp1fzo  13771  zpnn0elfzo  13777  elfzom1elp1fzo1  13806  fzonfzoufzol  13809  quoremnn0  13896  zmodidfzoimp  13941  modabs  13944  modifeq2int  13974  modaddmulmod  13979  expcl2lem  14114  hashgt23el  14463  hashreshashfun  14478  iswrdsymb  14569  ccatcl  14612  ccatsymb  14620  swrdfv2  14699  swrdsbslen  14702  swrdspsleq  14703  pfxswrd  14744  pfxccatin12lem3  14770  pfxccatpfx2  14775  swrdccat3blem  14777  reuccatpfxs1  14785  repswccat  14824  cshweqdifid  14858  lswco  14878  repsco  14879  s4f1o  14957  trclun  15053  mulre  15160  rediv  15170  imdiv  15177  resqrex  15289  caurcvg2  15714  fsumdifsnconst  15827  modfsummods  15829  tanval  16164  p1modz1  16297  negdvdsb  16310  muldvds1  16318  muldvds2  16319  dvdscmulr  16322  dvdsmulcr  16323  sumodd  16425  divalglem8  16437  divgcdnn  16552  lcmfunsnlem2lem2  16676  lcmfun  16682  2mulprm  16730  maxprmfct  16746  vfermltlALT  16840  modprm0  16843  pcpremul  16881  pcmul  16889  oddprmdvds  16941  prmdvdsprmo  17080  cshwsidrepsw  17131  gsumccat  18854  grpissubg  19164  ecqusaddd  19210  ecqusaddcl  19211  eqg0subg  19214  gim0to0  19287  gsmsymgreqlem2  19449  symgfixfo  19457  fsfnn0gsumfsffz  20001  rnglz  20162  isringrng  20284  irredn0  20423  c0snmgmhm  20462  rimisrngim  20498  zrrnghm  20536  rnghmsubcsetclem2  20632  rhmsubcsetclem2  20661  rhmsubcrngclem2  20667  lsppratlem1  21149  qusmulrng  21292  quscrng  21293  rngqiprngghmlem3  21299  rngqiprnglinlem3  21303  rngqiprngimf1lem  21304  rngqiprnglin  21312  cnfldfunALT  21379  cnfldfunALTOLD  21392  dvdsrzring  21472  mpofrlmd  21797  matinvgcell  22441  mat1dimcrng  22483  dmatscmcl  22509  scmatscm  22519  scmatghm  22539  scmatmhm  22540  ma1repvcl  22576  slesolinv  22686  slesolinvbi  22687  cramerimplem1  22689  cramerimp  22692  cramerlem1  22693  cramer  22697  cpmatacl  22722  cpmatmcl  22725  mat2pmatghm  22736  mat2pmatmul  22737  m2pmfzgsumcl  22754  decpmatmul  22778  decpmatmulsumfsupp  22779  pmatcollpwfi  22788  pm2mpf1  22805  pm2mpghm  22822  pm2mpmhmlem1  22824  monmat2matmon  22830  chpdmatlem2  22845  chpdmat  22847  cpmadugsumlemB  22880  cpmadugsumlemC  22881  cpmadugsumlemF  22882  clscld  23055  neiptopnei  23140  2ndcdisj2  23465  comppfsc  23540  tx1stc  23658  opnfbas  23850  fbasfip  23876  alexsublem  24052  alexsubALTlem4  24058  cnextcn  24075  ngpocelbl  24725  cphipval  25277  bcthlem5  25362  vitalilem4  25646  vitalilem5  25647  itg2mulc  25782  bddiblnc  25877  dvcobr  25983  dvcobrOLD  25984  dvcnvlem  26014  dvferm1  26023  dvne0  26050  mdegmullem  26117  plyeq0lem  26249  plyexmo  26355  aalioulem5  26378  aalioulem6  26379  aaliou  26380  cxple2a  26741  cxpaddlelem  26794  cxpaddle  26795  relogbcxpb  26830  bcmono  27321  lgsprme0  27383  gausslemma2dlem0e  27404  gausslemma2dlem1a  27409  gausslemma2dlem6  27416  lgsquadlem2  27425  2lgsoddprm  27460  elno2  27699  cofcutr  27958  colinearalg  28925  axcontlem3  28981  umgrislfupgrlem  29139  edgupgr  29151  usgruspgrb  29200  usgrislfuspgr  29204  edgssv2  29215  umgr2edg  29226  uspgredg2v  29241  usgrexmplef  29276  subupgr  29304  subusgr  29306  nbupgrres  29381  nb3gr2nb  29401  nbupgruvtxres  29424  cusgrres  29466  cusgrsizeindslem  29469  cusgrsizeinds  29470  vtxdun  29499  finrusgrfusgr  29583  cusgrrusgr  29599  pthdifv  29750  spthdep  29754  cycliscrct  29819  crctcshwlkn0lem6  29835  crctcshwlkn0lem7  29836  crctcshtrl  29843  crctcsh  29844  umgr2adedgwlkonALT  29967  elwwlks2  29986  elwspths2spth  29987  rusgrnumwwlk  29995  clwlkclwwlklem2a  30017  clwlkclwwlklem3  30020  clwwisshclwws  30034  wwlksubclwwlk  30077  eleclclwwlknlem2  30080  eupth2lem3lem3  30249  eucrct2eupth1  30263  frgr3v  30294  3vfriswmgr  30297  1to3vfriswmgr  30299  3cyclfrgr  30307  vdgn1frgrv2  30315  frgrwopreglem5  30340  frgrwopreglem5ALT  30341  frrusgrord0lem  30358  frrusgrord0  30359  2clwwlk2clwwlk  30369  extwwlkfab  30371  numclwwlk1lem2fo  30377  friendshipgt3  30417  ex-natded9.20-2  30437  grpoidinvlem3  30525  grpoidinv  30527  nmobndseqi  30798  nmobndseqiALT  30799  hvaddsub4  31097  ocsh  31302  5oalem2  31674  5oalem5  31677  3oalem2  31682  pjjsi  31719  hoadddir  31823  leopmul  32153  stge1i  32257  hatomistici  32381  mdsymlem2  32423  mdsymlem5  32426  addltmulALT  32465  isoun  32711  fsumiunle  32831  lsmsnorb  33419  crefdf  33847  qqhre  34021  esumiun  34095  sxbrsigalem0  34273  dya2iocnei  34284  sxbrsigalem5  34290  sibfinima  34341  eulerpartlemgs2  34382  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemsup  34507  bnj529  34755  bnj945  34787  bnj1098  34797  bnj1533  34866  bnj605  34921  bnj594  34926  bnj607  34930  bnj966  34958  bnj967  34959  bnj996  34970  bnj999  34972  bnj1006  34974  bnj1118  34998  bnj1172  35015  bnj1279  35032  bnj1296  35035  bnj1498  35075  fnrelpredd  35103  lfuhgr3  35125  loop1cycl  35142  cvmsi  35270  satf0op  35382  satffunlem1lem1  35407  satffunlem2lem1  35409  fv2ndcnv  35778  trisegint  36029  funtransport  36032  btwnconn1lem4  36091  btwnconn2  36103  segcon2  36106  outsideofeu  36132  isfne  36340  lukshef-ax2  36416  limsucncmpi  36446  weiunso  36467  bj-nsnid  37071  bj-restn0b  37092  bj-eldiag2  37178  bj-isrvec2  37301  pibt2  37418  unccur  37610  lindsadd  37620  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem30  37657  poimirlem32  37659  heicant  37662  ismblfin  37668  itg2gt0cn  37682  areacirc  37720  opelopab3  37725  isdivrngo  37957  isdrngo2  37965  fldcrngo  38011  flddmn  38065  refrelredund4  38636  mainer2  38847  cmtbr4N  39256  linepsubN  39754  pmapsub  39770  paddasslem14  39835  pclcmpatN  39903  trlval2  40165  cdleme20  40326  cdleme21j  40338  dvalveclem  41027  dia2dimlem7  41072  dvhlveclem  41110  docaclN  41126  dihjat1  41431  mapdhcl  41729  mapdh6dN  41741  mapdh8  41790  hdmap1l6d  41815  hdmap10  41842  hdmaprnlem17N  41865  hdmaplkr  41915  hdmapip0  41917  hgmapvv  41928  aks6d1c4  42125  cmpfiiin  42708  pellexlem4  42843  pellqrex  42890  acongtr  42990  acongrep  42992  jm2.23  43008  omlimcl2  43254  onsucf1lem  43282  oege1  43319  nnoeomeqom  43325  cantnfresb  43337  onmcl  43344  tfsconcat0i  43358  ofoafg  43367  ofoafo  43369  ofoaass  43373  ofoacom  43374  naddcnfass  43382  rp-fakeanorass  43526  rp-isfinite6  43531  harval3  43551  inintabss  43591  rfovcnvf1od  44017  clsk1indlem3  44056  ntrclsk13  44084  pm10.55  44388  refsum2cnlem1  45042  axccd2  45235  mptssid  45247  fmuldfeq  45598  climsuse  45623  limclner  45666  climxlim2lem  45860  icccncfext  45902  stoweidlem26  46041  stoweidlem52  46067  stoweidlem57  46072  fourierdlem20  46142  fourierdlem41  46163  fourierdlem52  46173  fourierdlem64  46185  fourierdlem102  46223  fourierdlem114  46235  ovolval4lem1  46664  preimagelt  46714  preimalegt  46715  funressneu  47059  afvelrn  47180  elfz2z  47327  2ffzoeq  47339  zplusmodne  47345  addmodne  47346  minusmod5ne  47351  imasetpreimafvbijlemfv  47389  imasetpreimafvbijlemf1  47391  fargshiftfva  47430  ichreuopeq  47460  2exopprim  47512  reuopreuprim  47513  fmtnoprmfac1  47552  proththd  47601  opoeALTV  47670  evensumeven  47694  sbgoldbalt  47768  evengpop3  47785  evengpoap3  47786  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  tgoldbach  47804  dfclnbgr6  47842  dfsclnbgr6  47844  uspgrimprop  47873  isuspgrimlem  47874  gricushgr  47886  uhgrimisgrgric  47899  isubgr3stgrlem7  47939  uspgrlimlem2  47956  gpgedgvtx0  48019  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem3  48029  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  gpg5gricstgr3  48046  assintop  48125  uzlidlring  48151  2zrngnmrid  48172  cznrng  48177  lmodvsmdi  48295  lincsum  48346  lincsumcl  48348  el0ldep  48383  ldepspr  48390  lindssnlvec  48403  modn0mul  48441  m1modmmod  48442  nn0digval  48521  1arympt1fv  48560  eenglngeehlnmlem1  48658  rrx2linest  48663  line2  48673  itsclc0yqe  48682  r19.41dv  48722  setrec1lem3  49208  aacllem  49320