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  2568  r19.28v  3168  rmob  3853  eqeuel  4328  preq12nebg  4827  fores  6782  fdmeu  6917  ssimaex  6946  dffv2  6956  exfo  7077  fpropnf1  7242  f1ocoima  7278  oprabv  7449  ndmovass  7577  fun11uni  7909  resf1ext2b  7911  fabexgOLD  7915  f1oabexgOLD  7919  f1iun  7922  soxp  8108  tz7.48lem  8409  tz7.49c  8414  omass  8544  oewordri  8556  omabs  8615  sbthlem9  9059  pssnn  9132  fineqvlem  9209  domunfican  9272  fiint  9277  fiintOLD  9278  fsuppsssupp  9332  sup0  9418  inf1  9575  infeq5  9590  cantnfle  9624  rankuni  9816  djuunxp  9874  acndom  10004  acnnum  10005  cdainflem  10141  cfcof  10227  ac6num  10432  ac6s2  10439  brdom5  10482  brdom4  10483  genpnnp  10958  divmulasscom  11861  lediv2a  12077  supmul1  12152  infregelb  12167  nn2ge  12213  btwnz  12637  eluz2b2  12880  uz2mulcl  12885  eqreznegel  12893  xrsupexmnf  13265  xrinfmexpnf  13266  xrsupsslem  13267  xrinfmsslem  13268  supxrun  13276  ioo0  13331  elioo4g  13367  fz0fzelfz0  13595  fz0fzdiffz0  13598  2ffzeq  13610  elfzodifsumelfzo  13692  elfzom1elp1fzo  13693  zpnn0elfzo  13699  elfzom1elp1fzo1  13728  fzonfzoufzol  13731  quoremnn0  13818  zmodidfzoimp  13863  modabs  13866  modaddb  13871  modifeq2int  13898  modaddmulmod  13903  expcl2lem  14038  hashgt23el  14389  hashreshashfun  14404  iswrdsymb  14496  ccatcl  14539  ccatsymb  14547  swrdfv2  14626  swrdsbslen  14629  swrdspsleq  14630  pfxswrd  14671  pfxccatin12lem3  14697  pfxccatpfx2  14702  swrdccat3blem  14704  reuccatpfxs1  14712  repswccat  14751  cshweqdifid  14785  lswco  14805  repsco  14806  s4f1o  14884  trclun  14980  mulre  15087  rediv  15097  imdiv  15104  resqrex  15216  caurcvg2  15644  fsumdifsnconst  15757  modfsummods  15759  tanval  16096  p1modz1  16229  negdvdsb  16242  muldvds1  16250  muldvds2  16251  dvdscmulr  16254  dvdsmulcr  16255  sumodd  16358  divalglem8  16370  divgcdnn  16485  lcmfunsnlem2lem2  16609  lcmfun  16615  2mulprm  16663  maxprmfct  16679  vfermltlALT  16773  modprm0  16776  pcpremul  16814  pcmul  16822  oddprmdvds  16874  prmdvdsprmo  17013  cshwsidrepsw  17064  gsumccat  18768  grpissubg  19078  ecqusaddd  19124  ecqusaddcl  19125  eqg0subg  19128  gim0to0  19201  gsmsymgreqlem2  19361  symgfixfo  19369  fsfnn0gsumfsffz  19913  rnglz  20074  isringrng  20196  irredn0  20332  c0snmgmhm  20371  rimisrngim  20407  zrrnghm  20445  rnghmsubcsetclem2  20541  rhmsubcsetclem2  20570  rhmsubcrngclem2  20576  lsppratlem1  21057  qusmulrng  21192  quscrng  21193  rngqiprngghmlem3  21199  rngqiprnglinlem3  21203  rngqiprngimf1lem  21204  rngqiprnglin  21212  cnfldfunALT  21279  cnfldfunALTOLD  21292  dvdsrzring  21371  mpofrlmd  21686  matinvgcell  22322  mat1dimcrng  22364  dmatscmcl  22390  scmatscm  22400  scmatghm  22420  scmatmhm  22421  ma1repvcl  22457  slesolinv  22567  slesolinvbi  22568  cramerimplem1  22570  cramerimp  22573  cramerlem1  22574  cramer  22578  cpmatacl  22603  cpmatmcl  22606  mat2pmatghm  22617  mat2pmatmul  22618  m2pmfzgsumcl  22635  decpmatmul  22659  decpmatmulsumfsupp  22660  pmatcollpwfi  22669  pm2mpf1  22686  pm2mpghm  22703  pm2mpmhmlem1  22705  monmat2matmon  22711  chpdmatlem2  22726  chpdmat  22728  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  clscld  22934  neiptopnei  23019  2ndcdisj2  23344  comppfsc  23419  tx1stc  23537  opnfbas  23729  fbasfip  23755  alexsublem  23931  alexsubALTlem4  23937  cnextcn  23954  ngpocelbl  24592  cphipval  25143  bcthlem5  25228  vitalilem4  25512  vitalilem5  25513  itg2mulc  25648  bddiblnc  25743  dvcobr  25849  dvcobrOLD  25850  dvcnvlem  25880  dvferm1  25889  dvne0  25916  mdegmullem  25983  plyeq0lem  26115  plyexmo  26221  aalioulem5  26244  aalioulem6  26245  aaliou  26246  cxple2a  26608  cxpaddlelem  26661  cxpaddle  26662  relogbcxpb  26697  bcmono  27188  lgsprme0  27250  gausslemma2dlem0e  27271  gausslemma2dlem1a  27276  gausslemma2dlem6  27283  lgsquadlem2  27292  2lgsoddprm  27327  elno2  27566  cofcutr  27832  colinearalg  28837  axcontlem3  28893  umgrislfupgrlem  29049  edgupgr  29061  usgruspgrb  29110  usgrislfuspgr  29114  edgssv2  29125  umgr2edg  29136  uspgredg2v  29151  usgrexmplef  29186  subupgr  29214  subusgr  29216  nbupgrres  29291  nb3gr2nb  29311  nbupgruvtxres  29334  cusgrres  29376  cusgrsizeindslem  29379  cusgrsizeinds  29380  vtxdun  29409  finrusgrfusgr  29493  cusgrrusgr  29509  pthdifv  29660  spthdep  29664  cycliscrct  29729  crctcshwlkn0lem6  29745  crctcshwlkn0lem7  29746  crctcshtrl  29753  crctcsh  29754  umgr2adedgwlkonALT  29877  elwwlks2  29896  elwspths2spth  29897  rusgrnumwwlk  29905  clwlkclwwlklem2a  29927  clwlkclwwlklem3  29930  clwwisshclwws  29944  wwlksubclwwlk  29987  eleclclwwlknlem2  29990  eupth2lem3lem3  30159  eucrct2eupth1  30173  frgr3v  30204  3vfriswmgr  30207  1to3vfriswmgr  30209  3cyclfrgr  30217  vdgn1frgrv2  30225  frgrwopreglem5  30250  frgrwopreglem5ALT  30251  frrusgrord0lem  30268  frrusgrord0  30269  2clwwlk2clwwlk  30279  extwwlkfab  30281  numclwwlk1lem2fo  30287  friendshipgt3  30327  ex-natded9.20-2  30347  grpoidinvlem3  30435  grpoidinv  30437  nmobndseqi  30708  nmobndseqiALT  30709  hvaddsub4  31007  ocsh  31212  5oalem2  31584  5oalem5  31587  3oalem2  31592  pjjsi  31629  hoadddir  31733  leopmul  32063  stge1i  32167  hatomistici  32291  mdsymlem2  32333  mdsymlem5  32336  addltmulALT  32375  isoun  32625  fsumiunle  32754  lsmsnorb  33362  crefdf  33838  qqhre  34010  esumiun  34084  sxbrsigalem0  34262  dya2iocnei  34273  sxbrsigalem5  34279  sibfinima  34330  eulerpartlemgs2  34371  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemsup  34496  bnj529  34731  bnj945  34763  bnj1098  34773  bnj1533  34842  bnj605  34897  bnj594  34902  bnj607  34906  bnj966  34934  bnj967  34935  bnj996  34946  bnj999  34948  bnj1006  34950  bnj1118  34974  bnj1172  34991  bnj1279  35008  bnj1296  35011  bnj1498  35051  fnrelpredd  35079  lfuhgr3  35107  loop1cycl  35124  cvmsi  35252  satf0op  35364  satffunlem1lem1  35389  satffunlem2lem1  35391  fv2ndcnv  35765  trisegint  36016  funtransport  36019  btwnconn1lem4  36078  btwnconn2  36090  segcon2  36093  outsideofeu  36119  isfne  36327  lukshef-ax2  36403  limsucncmpi  36433  weiunso  36454  bj-nsnid  37058  bj-restn0b  37079  bj-eldiag2  37165  bj-isrvec2  37288  pibt2  37405  unccur  37597  lindsadd  37607  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem30  37644  poimirlem32  37646  heicant  37649  ismblfin  37655  itg2gt0cn  37669  areacirc  37707  opelopab3  37712  isdivrngo  37944  isdrngo2  37952  fldcrngo  37998  flddmn  38052  refrelredund4  38626  mainer2  38838  cmtbr4N  39248  linepsubN  39746  pmapsub  39762  paddasslem14  39827  pclcmpatN  39895  trlval2  40157  cdleme20  40318  cdleme21j  40330  dvalveclem  41019  dia2dimlem7  41064  dvhlveclem  41102  docaclN  41118  dihjat1  41423  mapdhcl  41721  mapdh6dN  41733  mapdh8  41782  hdmap1l6d  41807  hdmap10  41834  hdmaprnlem17N  41857  hdmaplkr  41907  hdmapip0  41909  hgmapvv  41920  aks6d1c4  42112  cmpfiiin  42685  pellexlem4  42820  pellqrex  42867  acongtr  42967  acongrep  42969  jm2.23  42985  omlimcl2  43231  onsucf1lem  43258  oege1  43295  nnoeomeqom  43301  cantnfresb  43313  onmcl  43320  tfsconcat0i  43334  ofoafg  43343  ofoafo  43345  ofoaass  43349  ofoacom  43350  naddcnfass  43358  rp-fakeanorass  43502  rp-isfinite6  43507  harval3  43527  inintabss  43567  rfovcnvf1od  43993  clsk1indlem3  44032  ntrclsk13  44060  pm10.55  44358  refsum2cnlem1  45031  axccd2  45224  mptssid  45235  fmuldfeq  45581  climsuse  45606  limclner  45649  climxlim2lem  45843  icccncfext  45885  stoweidlem26  46024  stoweidlem52  46050  stoweidlem57  46055  fourierdlem20  46125  fourierdlem41  46146  fourierdlem52  46156  fourierdlem64  46168  fourierdlem102  46206  fourierdlem114  46218  ovolval4lem1  46647  preimagelt  46697  preimalegt  46698  squeezedltsq  46887  funressneu  47048  afvelrn  47169  elfz2z  47316  2ffzoeq  47328  zplusmodne  47344  addmodne  47345  minusmod5ne  47350  modn0mul  47358  m1modmmod  47359  imasetpreimafvbijlemfv  47403  imasetpreimafvbijlemf1  47405  fargshiftfva  47444  ichreuopeq  47474  2exopprim  47526  reuopreuprim  47527  fmtnoprmfac1  47566  proththd  47615  opoeALTV  47684  evensumeven  47708  sbgoldbalt  47782  evengpop3  47799  evengpoap3  47800  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  tgoldbach  47818  dfclnbgr6  47856  dfsclnbgr6  47858  uhgrimedg  47891  uhgrimprop  47892  isuspgrimlem  47895  isuspgrim  47896  gricushgr  47917  uhgrimisgrgric  47931  isubgr3stgrlem7  47971  uspgrlimlem2  47988  gpgedgel  48041  gpgprismgriedgdmss  48043  gpgedgvtx0  48052  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem3  48064  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  gpg5gricstgr3  48081  pgnbgreunbgrlem4  48109  assintop  48197  uzlidlring  48223  2zrngnmrid  48244  cznrng  48249  lmodvsmdi  48367  lincsum  48418  lincsumcl  48420  el0ldep  48455  ldepspr  48462  lindssnlvec  48475  nn0digval  48589  1arympt1fv  48628  eenglngeehlnmlem1  48726  rrx2linest  48731  line2  48741  itsclc0yqe  48750  r19.41dv  48790  setrec1lem3  49678  aacllem  49790