Theorem anim1i 592

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  sylanl1  682  sylanr1  684  disamis  2576  rmob  3529  eqeuel  3941  elpwdifsn  4319  fores  6124  ssimaex  6263  dffv2  6271  exfo  6377  frnssb  6391  fpropnf1  6524  oprabv  6703  ndmovass  6822  fun11uni  7120  fabexg  7122  f1oabexg  7125  fun11iun  7126  soxp  7290  tz7.48lem  7536  tz7.49c  7541  omass  7660  oewordri  7672  omabs  7727  sbthlem9  8078  fineqvlem  8174  pssnn  8178  domunfican  8233  fiint  8237  fsuppsssupp  8291  sup0  8372  inf1  8519  infeq5  8534  cantnfle  8568  rankuni  8726  acndom  8874  acnnum  8875  cdainflem  9013  cfcof  9096  ac6num  9301  ac6s2  9308  brdom5  9351  brdom4  9352  genpnnp  9827  divmulasscom  10709  lediv2a  10917  supmul1  10992  infregelb  11007  nn2ge  11045  btwnz  11479  eluz2b2  11761  uz2mulcl  11766  eqreznegel  11774  xrsupexmnf  12135  xrinfmexpnf  12136  xrsupsslem  12137  xrinfmsslem  12138  supxrun  12146  ioo0  12200  elioo4g  12234  fz0fzelfz0  12445  fz0fzdiffz0  12448  2ffzeq  12460  elfzodifsumelfzo  12533  elfzom1elp1fzo  12534  zpnn0elfzo  12540  elfzom1elp1fzo1  12568  fzonfzoufzol  12571  quoremnn0  12655  zmodidfzoimp  12700  modabs  12703  modmuladd  12712  modifeq2int  12732  modaddmulmod  12737  expcl2lem  12872  hashreshashfun  13226  iswrdsymb  13322  ccatcl  13359  ccatval3  13363  ccatalpha  13375  swrdfv2  13446  swrdsbslen  13448  swrdspsleq  13449  swrd0swrd  13461  swrdccatin2  13487  swrdccatin12lem3  13490  swrdccat3  13492  swrdccat3blem  13495  swrdccatid  13497  repswccat  13532  2cshw  13559  cshweqdifid  13566  lswco  13584  repsco  13585  s4f1o  13663  ccat2s1fvwALT  13698  trclun  13755  mulre  13861  rediv  13871  imdiv  13878  resqrex  13991  caurcvg2  14408  fsumdifsnconst  14523  modfsummods  14525  tanval  14858  negdvdsb  14998  muldvds1  15006  muldvds2  15007  dvdscmulr  15010  dvdsmulcr  15011  dvdsdivcl  15038  nn0ehalf  15095  nn0oddm1d2  15101  nnoddm1d2  15102  sumeven  15110  sumodd  15111  divalglem8  15123  divgcdnn  15236  lcmfunsnlem2lem2  15352  lcmfun  15358  coprmgcdb  15362  ncoprmgcdne1b  15363  divgcdcoprm0  15379  maxprmfct  15421  ncoprmlnprm  15436  vfermltl  15506  vfermltlALT  15507  modprm0  15510  modprmn0modprm0  15512  pcpremul  15548  pcmul  15556  dvdsprmpweqle  15590  oddprmdvds  15607  prmdvdsprmo  15746  prmgaplem4  15758  prmgaplem7  15761  cshwsidrepsw  15800  gsmsymgreqlem2  17851  symgfixfo  17859  fsfnn0gsumfsffz  18379  irredn0  18703  rim0to0  18742  lsppratlem1  19147  ixpsnbasval  19209  cply1coe0bi  19670  dvdsrzring  19831  matinvgcell  20241  mat1dimcrng  20283  dmatscmcl  20309  scmatmats  20317  scmatscm  20319  scmatmulcl  20324  scmatghm  20339  scmatmhm  20340  ma1repvcl  20376  mdet1  20407  mdet0  20412  slesolinv  20486  slesolinvbi  20487  cramerimplem1  20489  cramerimp  20492  cramerlem1  20493  cramer  20497  cpmatacl  20521  cpmatmcl  20524  mat2pmatghm  20535  mat2pmatmul  20536  m2pmfzgsumcl  20553  decpmatmul  20577  decpmatmulsumfsupp  20578  pmatcollpwfi  20587  pmatcollpwscmat  20596  pm2mpf1  20604  pm2mpghm  20621  pm2mpmhmlem1  20623  monmat2matmon  20629  chpdmatlem2  20644  chpdmat  20646  chfacfisf  20659  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  clscld  20851  neiptopnei  20936  2ndcdisj2  21260  comppfsc  21335  tx1stc  21453  opnfbas  21646  fbasfip  21672  alexsublem  21848  alexsubALTlem4  21854  cnextcn  21871  ngpocelbl  22508  cvsi  22930  cphipval  23042  bcthlem5  23125  vitalilem4  23380  vitalilem5  23381  itg2mulc  23514  dvcobr  23709  dvcnvlem  23739  dvferm1  23748  dvne0  23774  mdegmullem  23838  plyeq0lem  23966  plyexmo  24068  aalioulem5  24091  aalioulem6  24092  aaliou  24093  cxple2a  24445  cxpaddlelem  24492  cxpaddle  24493  relogbcxpb  24525  bcmono  25002  lgsprme0  25064  gausslemma2dlem0e  25085  gausslemma2dlem1a  25090  gausslemma2dlem6  25097  lgsquadlem2  25106  2lgsoddprm  25141  colinearalg  25790  axcontlem3  25846  umgrislfupgrlem  26017  edgupgr  26029  usgruspgrb  26076  usgrislfuspgr  26079  edgssv2  26090  umgr2edg  26101  usgr2edg  26102  uspgredg2v  26116  usgrexmplef  26151  subupgr  26179  subusgr  26181  usgrfilem  26219  nbupgrres  26266  nb3gr2nb  26286  nbupgruvtxres  26308  cplgr3v  26331  cusgrres  26344  cusgrsizeindslem  26347  cusgrsizeinds  26348  vtxdun  26377  finrusgrfusgr  26461  cusgrrusgr  26477  wlkonprop  26554  wlkreslem  26566  trlsonprop  26604  spthdep  26630  pthsonprop  26640  spthonprop  26641  cycliscrct  26694  crctcshwlkn0lem6  26707  crctcshwlkn0lem7  26708  crctcshtrl  26715  crctcsh  26716  wlkwwlksur  26783  umgr2adedgwlkonALT  26843  elwwlks2  26861  elwspths2spth  26862  rusgrnumwwlk  26870  clwwlknbp0  26884  clwlkclwwlklem2a  26899  clwlkclwwlklem3  26902  clwwlksnfi  26913  wwlksext2clwwlk  26924  wwlksubclwwlks  26925  clwwisshclwws  26928  eleclclwwlksnlem2  26939  clwlksfclwwlk  26962  clwlksf1clwwlklem0  26964  uhgr3cyclex  27042  eupth2lem3lem3  27090  eucrctshift  27103  eucrct2eupth1  27104  frgr3v  27139  3vfriswmgr  27142  1to3vfriswmgr  27144  3cyclfrgr  27152  frgrnbnb  27157  vdgn1frgrv2  27160  frgrwopreglem5  27185  frgrwopreglem5ALT  27186  fusgreghash2wspv  27199  frrusgrord0lem  27203  frrusgrord0  27204  extwwlkfablem2  27210  numclwwlk4  27244  numclwwlk6  27248  frgrreggt1  27251  friendshipgt3  27256  ex-natded9.20-2  27275  grpoidinvlem3  27360  grpoidinv  27362  nmobndseqi  27634  nmobndseqiALT  27635  hvaddsub4  27935  hhcmpl  28057  ocsh  28142  5oalem2  28514  5oalem5  28517  3oalem2  28522  pjjsi  28559  hoadddir  28663  leopmul  28993  stge1i  29097  hatomistici  29221  mdsymlem2  29263  mdsymlem5  29266  addltmulALT  29305  isoun  29479  fsumiunle  29575  crefdf  29915  qqhre  30064  esumiun  30156  sxbrsigalem0  30333  dya2iocnei  30344  sxbrsigalem5  30350  sibfinima  30401  eulerpartlemgs2  30442  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemsup  30566  bnj529  30811  bnj945  30844  bnj1098  30854  bnj1533  30922  bnj605  30977  bnj594  30982  bnj607  30986  bnj966  31014  bnj967  31015  bnj996  31025  bnj999  31027  bnj1006  31029  bnj1118  31052  bnj1172  31069  bnj1279  31086  bnj1296  31089  bnj1498  31129  cvmsi  31247  fv2ndcnv  31681  elno2  31807  trisegint  32135  funtransport  32138  btwnconn1lem4  32197  btwnconn2  32209  segcon2  32212  outsideofeu  32238  isfne  32334  lukshef-ax2  32414  limsucncmpi  32444  bj-restn0b  33044  bj-elid3  33087  bj-eldiag2  33092  unccur  33392  lindsenlbs  33404  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem30  33439  poimirlem32  33441  heicant  33444  ismblfin  33450  itg2gt0cn  33465  bddiblnc  33480  areacirc  33505  opelopab3  33511  isdivrngo  33749  isdrngo2  33757  fldcrng  33803  flddmn  33857  cmtbr4N  34542  linepsubN  35038  pmapsub  35054  paddasslem14  35119  pclcmpatN  35187  trlval2  35450  cdleme20  35612  cdleme21j  35624  dvalveclem  36314  dia2dimlem7  36359  dvhlveclem  36397  docaclN  36413  dihjat1  36718  mapdhcl  37016  mapdh6dN  37028  mapdh8  37078  hdmap1l6d  37103  hdmap10  37132  hdmaprnlem17N  37155  hdmaplkr  37205  hdmapip0  37207  hgmapvv  37218  cmpfiiin  37260  pellexlem4  37396  pellqrex  37443  acongtr  37545  acongrep  37547  jm2.23  37563  rp-fakeanorass  37858  rp-isfinite6  37864  inintabss  37884  rfovcnvf1od  38298  clsk1indlem3  38341  ntrclsk13  38369  pm10.55  38568  refsum2cnlem1  39196  axccd2  39430  fmuldfeq  39815  climsuse  39840  limclner  39883  climxlim2lem  40071  icccncfext  40100  stoweidlem26  40243  stoweidlem52  40269  stoweidlem57  40274  fourierdlem20  40344  fourierdlem41  40365  fourierdlem52  40375  fourierdlem64  40387  fourierdlem102  40425  fourierdlem114  40437  ovolval4lem1  40863  preimagelt  40912  preimalegt  40913  afvelrn  41248  elfz2z  41325  2ffzoeq  41338  fargshiftfva  41379  ccatpfx  41409  pfxccat3  41426  pfxccatpfx2  41428  pfxccat3a  41429  reuccatpfxs1  41434  fmtnoprmfac1  41477  proththd  41531  opoeALTV  41594  evensumeven  41616  sbgoldbalt  41669  evengpop3  41686  evengpoap3  41687  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  tgoldbach  41705  tgoldbachOLD  41712  uspgrsprfo  41756  assintop  41845  isringrng  41881  rnglz  41884  c0snmgmhm  41914  zrrnghm  41917  uzlidlring  41929  2zrngnmrid  41950  cznrng  41955  rnghmsubcsetclem2  41976  rhmsubcsetclem2  42022  rhmsubcrngclem2  42028  lmodvsmdi  42163  lincsum  42218  lincsumcl  42220  el0ldep  42255  ldepspr  42262  lindssnlvec  42275  modn0mul  42315  m1modmmod  42316  elbigolo1  42351  nn0digval  42394  setrec1lem3  42436  aacllem  42547