Theorem anim1i 590

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  sylanl1  680  sylanr1  682  disamis  2564  rmob  3495  fores  6037  ssimaex  6173  dffv2  6181  exfo  6285  frnssb  6298  oprabv  6601  ndmovass  6720  fun11uni  7013  fabexg  7015  f1oabexg  7018  fun11iun  7019  soxp  7177  tz7.48lem  7423  tz7.49c  7428  omass  7547  oewordri  7559  omabs  7614  sbthlem9  7963  fineqvlem  8059  pssnn  8063  domunfican  8118  fiint  8122  fsuppsssupp  8174  sup0  8255  inf1  8402  infeq5  8417  cantnfle  8451  rankuni  8609  acndom  8757  acnnum  8758  cdainflem  8896  cfcof  8979  ac6num  9184  ac6s2  9191  brdom5  9232  brdom4  9233  genpnnp  9706  divmulasscom  10588  lediv2a  10796  supmul1  10869  infregelb  10884  nn2ge  10922  btwnz  11355  eluz2b2  11637  uz2mulcl  11642  eqreznegel  11650  xrsupexmnf  12007  xrinfmexpnf  12008  xrsupsslem  12009  xrinfmsslem  12010  supxrun  12018  ioo0  12071  elioo4g  12105  fz0fzelfz0  12314  fz0fzdiffz0  12317  2ffzeq  12329  elfzodifsumelfzo  12401  elfzom1elp1fzo  12402  zpnn0elfzo  12407  elfzom1elp1fzo1  12434  fzonfzoufzol  12437  quoremnn0  12517  zmodidfzoimp  12562  modabs  12565  modmuladd  12574  modifeq2int  12594  modaddmulmod  12599  expcl2lem  12734  iswrdsymb  13177  ccatcl  13212  ccatval3  13216  ccatalpha  13228  swrdfv2  13298  swrdsbslen  13300  swrdspsleq  13301  swrd0swrd  13313  swrdccatin2  13338  swrdccatin12lem3  13341  swrdccat3  13343  swrdccat3blem  13346  swrdccatid  13348  repswccat  13383  2cshw  13410  cshweqdifid  13417  lswco  13435  repsco  13436  s4f1o  13513  ccat2s1fvwALT  13546  trclun  13603  mulre  13709  rediv  13719  imdiv  13726  resqrex  13839  caurcvg2  14256  modfsummods  14366  tanval  14697  negdvdsb  14836  muldvds1  14844  muldvds2  14845  dvdscmulr  14848  dvdsmulcr  14849  dvdsdivcl  14876  nn0ehalf  14933  nn0oddm1d2  14939  nnoddm1d2  14940  sumeven  14948  sumodd  14949  divalglem8  14961  divgcdnn  15074  lcmfunsnlem2lem2  15190  lcmfun  15196  coprmgcdb  15200  ncoprmgcdne1b  15201  divgcdcoprm0  15217  maxprmfct  15259  ncoprmlnprm  15274  vfermltl  15344  vfermltlALT  15345  modprm0  15348  modprmn0modprm0  15350  pcpremul  15386  pcmul  15394  dvdsprmpweqle  15428  oddprmdvds  15445  prmdvdsprmo  15584  prmgaplem4  15596  prmgaplem7  15599  cshwsidrepsw  15638  gsmsymgreqlem2  17674  symgfixfo  17682  fsfnn0gsumfsffz  18202  irredn0  18526  rim0to0  18565  lsppratlem1  18968  ixpsnbasval  19030  cply1coe0bi  19491  dvdsrzring  19650  matinvgcell  20060  mat1dimcrng  20102  dmatscmcl  20128  scmatmats  20136  scmatscm  20138  scmatmulcl  20143  scmatghm  20158  scmatmhm  20159  ma1repvcl  20195  mdet1  20226  mdet0  20231  slesolinv  20305  slesolinvbi  20306  cramerimplem1  20308  cramerimp  20311  cramerlem1  20312  cramer  20316  cpmatacl  20340  cpmatmcl  20343  mat2pmatghm  20354  mat2pmatmul  20355  m2pmfzgsumcl  20372  decpmatmul  20396  decpmatmulsumfsupp  20397  pmatcollpwfi  20406  pmatcollpwscmat  20415  pm2mpf1  20423  pm2mpghm  20440  pm2mpmhmlem1  20442  monmat2matmon  20448  chpdmatlem2  20463  chpdmat  20465  chfacfisf  20478  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  clscld  20661  neiptopnei  20746  2ndcdisj2  21070  comppfsc  21145  tx1stc  21263  opnfbas  21456  fbasfip  21482  alexsublem  21658  alexsubALTlem4  21664  cnextcn  21681  ngpocelbl  22318  cvsi  22738  cphipval  22850  bcthlem5  22933  vitalilem4  23186  vitalilem5  23187  itg2mulc  23320  dvcobr  23515  dvcnvlem  23543  dvferm1  23552  dvne0  23578  mdegmullem  23642  plyeq0lem  23770  plyexmo  23872  aalioulem5  23895  aalioulem6  23896  aaliou  23897  cxple2a  24245  cxpaddlelem  24292  cxpaddle  24293  relogbcxpb  24325  bcmono  24802  lgsprme0  24864  gausslemma2dlem0e  24885  gausslemma2dlem1a  24890  gausslemma2dlem6  24897  lgsquadlem2  24906  2lgsoddprm  24941  colinearalg  25590  axcontlem3  25646  uhgrstrrepelem  25744  umgrislfupgrlem  25788  edgupgr  25808  usgraexmplef  25929  nb3grapr  25982  nb3grapr2  25983  nb3gra2nb  25984  cusgrarn  25988  cusgrasizeindslem2  26003  spthonepeq  26117  fargshiftfva  26167  wlkiswwlksur  26247  clwwlknimp  26304  clwlkisclwwlklem2a  26313  clwlkisclwwlklem0  26316  wwlksubclwwlk  26332  clwwisshclww  26335  clwwnisshclwwn  26337  eleclclwwlknlem2  26346  usg2spthonot1  26417  vdusgraval  26434  cusgraisrusgra  26465  rusgranumwlk  26484  eupatrl  26495  1to3vfriswmgra  26534  frgranbnb  26547  vdfrgra0  26549  vdgn0frgrav2  26551  vdgn1frgrav2  26553  frgrawopreg  26576  frg2wot1  26584  usg2spot2nb  26592  frgraregorufrg  26599  numclwwlkovfel2  26610  numclwlk1lem2foa  26618  numclwlk1lem2fv  26620  numclwwlk1  26625  numclwlk2lem2fv  26631  numclwwlk4  26637  numclwwlk5  26639  numclwwlk6  26640  frgrareg  26644  frgraregord013  26645  ex-natded9.20-2  26667  grpoidinvlem3  26744  grpoidinv  26746  nmobndseqi  27018  nmobndseqiALT  27019  hvaddsub4  27319  hhcmpl  27441  ocsh  27526  5oalem2  27898  5oalem5  27901  3oalem2  27906  pjjsi  27943  hoadddir  28047  leopmul  28377  stge1i  28481  hatomistici  28605  mdsymlem2  28647  mdsymlem5  28650  addltmulALT  28689  isoun  28862  crefdf  29243  qqhre  29392  esumiun  29483  sxbrsigalem0  29660  dya2iocnei  29671  sxbrsigalem5  29677  sibfinima  29728  eulerpartlemgs2  29769  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemsup  29893  bnj529  30065  bnj945  30098  bnj1098  30108  bnj1533  30176  bnj605  30231  bnj594  30236  bnj607  30240  bnj966  30268  bnj967  30269  bnj996  30279  bnj999  30281  bnj1006  30283  bnj1118  30306  bnj1172  30323  bnj1279  30340  bnj1296  30343  bnj1498  30383  cvmsi  30501  fv2ndcnv  30926  elno2  31051  nobndlem6  31096  trisegint  31305  funtransport  31308  btwnconn1lem4  31367  btwnconn2  31379  segcon2  31382  outsideofeu  31408  isfne  31504  lukshef-ax2  31584  limsucncmpi  31614  bj-restn0b  32225  bj-elid3  32264  bj-eldiag2  32269  unccur  32562  lindsenlbs  32574  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  poimirlem30  32609  poimirlem32  32611  heicant  32614  ismblfin  32620  itg2gt0cn  32635  bddiblnc  32650  areacirc  32675  opelopab3  32681  isdivrngo  32919  isdrngo2  32927  fldcrng  32973  flddmn  33027  cmtbr4N  33560  linepsubN  34056  pmapsub  34072  paddasslem14  34137  pclcmpatN  34205  trlval2  34468  cdleme20  34630  cdleme21j  34642  dvalveclem  35332  dia2dimlem7  35377  dvhlveclem  35415  docaclN  35431  dihjat1  35736  mapdhcl  36034  mapdh6dN  36046  mapdh8  36096  hdmap1l6d  36121  hdmap10  36150  hdmaprnlem17N  36173  hdmaplkr  36223  hdmapip0  36225  hgmapvv  36236  cmpfiiin  36278  pellexlem4  36414  pellqrex  36461  acongtr  36563  acongrep  36565  jm2.23  36581  rp-fakeanorass  36877  rp-isfinite6  36883  inintabss  36903  rfovcnvf1od  37318  clsk1indlem3  37361  ntrclsk13  37389  pm10.55  37590  refsum2cnlem1  38219  axccd2  38425  fmuldfeq  38650  climsuse  38675  limclner  38718  icccncfext  38773  stoweidlem26  38919  stoweidlem52  38945  stoweidlem57  38950  fourierdlem20  39020  fourierdlem41  39041  fourierdlem52  39051  fourierdlem64  39063  fourierdlem102  39101  fourierdlem114  39113  ovolval4lem1  39539  preimagelt  39589  preimalegt  39590  afvelrn  39897  fmtnoprmfac1  40015  proththd  40069  opoeALTV  40132  evensumeven  40154  sgoldbalt  40203  evengpop3  40214  evengpoap3  40215  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  tgoldbach  40232  tgoldbachOLD  40239  ccatpfx  40272  pfxccat3  40289  pfxccatpfx2  40291  pfxccat3a  40292  reuccatpfxs1  40297  elpwdifsn  40312  fpropnf1  40337  elfz2z  40352  2ffzoeq  40361  usgruspgrb  40411  usgrislfuspgr  40414  edgassv2  40425  umgr2edg  40436  usgr2edg  40437  uspgredg2v  40451  subupgr  40511  subusgr  40513  usgrfilem  40546  nbupgrres  40592  nb3gr2nb  40612  nbupgruvtxres  40634  cplgr3v  40657  cusgrres  40664  cusgrsizeindslem  40667  cusgrsizeinds  40668  vtxdun  40696  finrusgrfusgr  40765  cusgrrusgr  40781  wlkOnprop  40866  1wlkreslem  40878  trlsonprop  40915  spthdep  40940  pthsonprop  40950  spthonprop  40951  spthonepeq-av  40958  uhgr1wlkspth  40961  usgr2wlkspth  40965  crctcsh1wlkn0lem6  41018  crctcsh1wlkn0lem7  41019  crctcshtrl  41026  crctcsh  41027  wlkwwlksur  41094  umgr2adedgwlkonALT  41154  elwwlks2  41170  elwspths2spth  41171  rusgrnumwwlk  41178  clwwlknbp0  41192  clwlkclwwlklem2a  41207  clwlkclwwlklem3  41210  clwwlksnfi  41220  wwlksext2clwwlk  41231  wwlksubclwwlks  41232  clwwisshclwws  41235  eleclclwwlksnlem2  41246  clwlksfclwwlk  41269  clwlksf1clwwlklem0  41271  uhgr3cyclex  41349  eupth2lem3lem3  41398  eucrctshift  41411  eucrct2eupth1  41412  frgr3v  41445  3vfriswmgr  41448  1to3vfriswmgr  41450  3cyclfrgr  41458  frgrnbnb  41463  vdgn1frgrv2  41466  frgrwopreg  41486  fusgr2wsp2nb  41498  fusgreghash2wspv  41499  frrusgrord0  41503  frgrregorufrg  41505  av-numclwlk1lem2foa  41521  av-numclwwlk4  41540  av-numclwwlk6  41544  av-frgrareggt1  41547  av-friendshipgt3  41552  assintop  41635  isringrng  41671  rnglz  41674  c0snmgmhm  41704  zrrnghm  41707  uzlidlring  41719  2zrngnmrid  41740  cznrng  41747  rnghmsubcsetclem2  41768  rhmsubcsetclem2  41814  rhmsubcrngclem2  41820  lmodvsmdi  41957  lincsum  42012  lincsumcl  42014  el0ldep  42049  ldepspr  42056  lindssnlvec  42069  modn0mul  42109  m1modmmod  42110  elbigolo1  42149  nn0digval  42192  setrec1lem3  42235  aacllem  42356