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  3160  rmob  3844  eqeuel  4318  preq12nebg  4817  fores  6750  fdmeu  6883  ssimaex  6912  dffv2  6922  exfo  7043  fpropnf1  7208  f1ocoima  7244  oprabv  7413  ndmovass  7541  fun11uni  7873  resf1ext2b  7875  fabexgOLD  7879  f1oabexgOLD  7883  f1iun  7886  soxp  8069  tz7.48lem  8370  tz7.49c  8375  omass  8505  oewordri  8517  omabs  8576  sbthlem9  9019  pssnn  9092  fineqvlem  9167  domunfican  9230  fiint  9235  fiintOLD  9236  fsuppsssupp  9290  sup0  9376  inf1  9537  infeq5  9552  cantnfle  9586  rankuni  9778  djuunxp  9836  acndom  9964  acnnum  9965  cdainflem  10101  cfcof  10187  ac6num  10392  ac6s2  10399  brdom5  10442  brdom4  10443  genpnnp  10918  divmulasscom  11821  lediv2a  12037  supmul1  12112  infregelb  12127  nn2ge  12173  btwnz  12597  eluz2b2  12840  uz2mulcl  12845  eqreznegel  12853  xrsupexmnf  13225  xrinfmexpnf  13226  xrsupsslem  13227  xrinfmsslem  13228  supxrun  13236  ioo0  13291  elioo4g  13327  fz0fzelfz0  13555  fz0fzdiffz0  13558  2ffzeq  13570  elfzodifsumelfzo  13652  elfzom1elp1fzo  13653  zpnn0elfzo  13659  elfzom1elp1fzo1  13688  fzonfzoufzol  13691  quoremnn0  13778  zmodidfzoimp  13823  modabs  13826  modaddb  13831  modifeq2int  13858  modaddmulmod  13863  expcl2lem  13998  hashgt23el  14349  hashreshashfun  14364  iswrdsymb  14456  ccatcl  14499  ccatsymb  14507  swrdfv2  14586  swrdsbslen  14589  swrdspsleq  14590  pfxswrd  14630  pfxccatin12lem3  14656  pfxccatpfx2  14661  swrdccat3blem  14663  reuccatpfxs1  14671  repswccat  14710  cshweqdifid  14744  lswco  14764  repsco  14765  s4f1o  14843  trclun  14939  mulre  15046  rediv  15056  imdiv  15063  resqrex  15175  caurcvg2  15603  fsumdifsnconst  15716  modfsummods  15718  tanval  16055  p1modz1  16188  negdvdsb  16201  muldvds1  16209  muldvds2  16210  dvdscmulr  16213  dvdsmulcr  16214  sumodd  16317  divalglem8  16329  divgcdnn  16444  lcmfunsnlem2lem2  16568  lcmfun  16574  2mulprm  16622  maxprmfct  16638  vfermltlALT  16732  modprm0  16735  pcpremul  16773  pcmul  16781  oddprmdvds  16833  prmdvdsprmo  16972  cshwsidrepsw  17023  gsumccat  18733  grpissubg  19043  ecqusaddd  19089  ecqusaddcl  19090  eqg0subg  19093  gim0to0  19166  gsmsymgreqlem2  19328  symgfixfo  19336  fsfnn0gsumfsffz  19880  rnglz  20068  isringrng  20190  irredn0  20326  c0snmgmhm  20365  rimisrngim  20401  zrrnghm  20439  rnghmsubcsetclem2  20535  rhmsubcsetclem2  20564  rhmsubcrngclem2  20570  lsppratlem1  21072  qusmulrng  21207  quscrng  21208  rngqiprngghmlem3  21214  rngqiprnglinlem3  21218  rngqiprngimf1lem  21219  rngqiprnglin  21227  cnfldfunALT  21294  cnfldfunALTOLD  21307  dvdsrzring  21386  mpofrlmd  21702  matinvgcell  22338  mat1dimcrng  22380  dmatscmcl  22406  scmatscm  22416  scmatghm  22436  scmatmhm  22437  ma1repvcl  22473  slesolinv  22583  slesolinvbi  22584  cramerimplem1  22586  cramerimp  22589  cramerlem1  22590  cramer  22594  cpmatacl  22619  cpmatmcl  22622  mat2pmatghm  22633  mat2pmatmul  22634  m2pmfzgsumcl  22651  decpmatmul  22675  decpmatmulsumfsupp  22676  pmatcollpwfi  22685  pm2mpf1  22702  pm2mpghm  22719  pm2mpmhmlem1  22721  monmat2matmon  22727  chpdmatlem2  22742  chpdmat  22744  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  clscld  22950  neiptopnei  23035  2ndcdisj2  23360  comppfsc  23435  tx1stc  23553  opnfbas  23745  fbasfip  23771  alexsublem  23947  alexsubALTlem4  23953  cnextcn  23970  ngpocelbl  24608  cphipval  25159  bcthlem5  25244  vitalilem4  25528  vitalilem5  25529  itg2mulc  25664  bddiblnc  25759  dvcobr  25865  dvcobrOLD  25866  dvcnvlem  25896  dvferm1  25905  dvne0  25932  mdegmullem  25999  plyeq0lem  26131  plyexmo  26237  aalioulem5  26260  aalioulem6  26261  aaliou  26262  cxple2a  26624  cxpaddlelem  26677  cxpaddle  26678  relogbcxpb  26713  bcmono  27204  lgsprme0  27266  gausslemma2dlem0e  27287  gausslemma2dlem1a  27292  gausslemma2dlem6  27299  lgsquadlem2  27308  2lgsoddprm  27343  elno2  27582  cofcutr  27855  colinearalg  28873  axcontlem3  28929  umgrislfupgrlem  29085  edgupgr  29097  usgruspgrb  29146  usgrislfuspgr  29150  edgssv2  29161  umgr2edg  29172  uspgredg2v  29187  usgrexmplef  29222  subupgr  29250  subusgr  29252  nbupgrres  29327  nb3gr2nb  29347  nbupgruvtxres  29370  cusgrres  29412  cusgrsizeindslem  29415  cusgrsizeinds  29416  vtxdun  29445  finrusgrfusgr  29529  cusgrrusgr  29545  pthdifv  29693  spthdep  29697  cycliscrct  29762  crctcshwlkn0lem6  29778  crctcshwlkn0lem7  29779  crctcshtrl  29786  crctcsh  29787  umgr2adedgwlkonALT  29910  elwwlks2  29929  elwspths2spth  29930  rusgrnumwwlk  29938  clwlkclwwlklem2a  29960  clwlkclwwlklem3  29963  clwwisshclwws  29977  wwlksubclwwlk  30020  eleclclwwlknlem2  30023  eupth2lem3lem3  30192  eucrct2eupth1  30206  frgr3v  30237  3vfriswmgr  30240  1to3vfriswmgr  30242  3cyclfrgr  30250  vdgn1frgrv2  30258  frgrwopreglem5  30283  frgrwopreglem5ALT  30284  frrusgrord0lem  30301  frrusgrord0  30302  2clwwlk2clwwlk  30312  extwwlkfab  30314  numclwwlk1lem2fo  30320  friendshipgt3  30360  ex-natded9.20-2  30380  grpoidinvlem3  30468  grpoidinv  30470  nmobndseqi  30741  nmobndseqiALT  30742  hvaddsub4  31040  ocsh  31245  5oalem2  31617  5oalem5  31620  3oalem2  31625  pjjsi  31662  hoadddir  31766  leopmul  32096  stge1i  32200  hatomistici  32324  mdsymlem2  32366  mdsymlem5  32369  addltmulALT  32408  isoun  32658  fsumiunle  32787  lsmsnorb  33338  crefdf  33814  qqhre  33986  esumiun  34060  sxbrsigalem0  34238  dya2iocnei  34249  sxbrsigalem5  34255  sibfinima  34306  eulerpartlemgs2  34347  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemsup  34472  bnj529  34707  bnj945  34739  bnj1098  34749  bnj1533  34818  bnj605  34873  bnj594  34878  bnj607  34882  bnj966  34910  bnj967  34911  bnj996  34922  bnj999  34924  bnj1006  34926  bnj1118  34950  bnj1172  34967  bnj1279  34984  bnj1296  34987  bnj1498  35027  fnrelpredd  35055  lfuhgr3  35092  loop1cycl  35109  cvmsi  35237  satf0op  35349  satffunlem1lem1  35374  satffunlem2lem1  35376  fv2ndcnv  35750  trisegint  36001  funtransport  36004  btwnconn1lem4  36063  btwnconn2  36075  segcon2  36078  outsideofeu  36104  isfne  36312  lukshef-ax2  36388  limsucncmpi  36418  weiunso  36439  bj-nsnid  37043  bj-restn0b  37064  bj-eldiag2  37150  bj-isrvec2  37273  pibt2  37390  unccur  37582  lindsadd  37592  lindsenlbs  37594  matunitlindflem1  37595  matunitlindflem2  37596  poimirlem26  37625  poimirlem27  37626  poimirlem29  37628  poimirlem30  37629  poimirlem32  37631  heicant  37634  ismblfin  37640  itg2gt0cn  37654  areacirc  37692  opelopab3  37697  isdivrngo  37929  isdrngo2  37937  fldcrngo  37983  flddmn  38037  refrelredund4  38611  mainer2  38823  cmtbr4N  39233  linepsubN  39731  pmapsub  39747  paddasslem14  39812  pclcmpatN  39880  trlval2  40142  cdleme20  40303  cdleme21j  40315  dvalveclem  41004  dia2dimlem7  41049  dvhlveclem  41087  docaclN  41103  dihjat1  41408  mapdhcl  41706  mapdh6dN  41718  mapdh8  41767  hdmap1l6d  41792  hdmap10  41819  hdmaprnlem17N  41842  hdmaplkr  41892  hdmapip0  41894  hgmapvv  41905  aks6d1c4  42097  cmpfiiin  42670  pellexlem4  42805  pellqrex  42852  acongtr  42951  acongrep  42953  jm2.23  42969  omlimcl2  43215  onsucf1lem  43242  oege1  43279  nnoeomeqom  43285  cantnfresb  43297  onmcl  43304  tfsconcat0i  43318  ofoafg  43327  ofoafo  43329  ofoaass  43333  ofoacom  43334  naddcnfass  43342  rp-fakeanorass  43486  rp-isfinite6  43491  harval3  43511  inintabss  43551  rfovcnvf1od  43977  clsk1indlem3  44016  ntrclsk13  44044  pm10.55  44342  refsum2cnlem1  45015  axccd2  45208  mptssid  45219  fmuldfeq  45565  climsuse  45590  limclner  45633  climxlim2lem  45827  icccncfext  45869  stoweidlem26  46008  stoweidlem52  46034  stoweidlem57  46039  fourierdlem20  46109  fourierdlem41  46130  fourierdlem52  46140  fourierdlem64  46152  fourierdlem102  46190  fourierdlem114  46202  ovolval4lem1  46631  preimagelt  46681  preimalegt  46682  squeezedltsq  46871  funressneu  47032  afvelrn  47153  elfz2z  47300  2ffzoeq  47312  zplusmodne  47328  addmodne  47329  minusmod5ne  47334  modn0mul  47342  m1modmmod  47343  imasetpreimafvbijlemfv  47387  imasetpreimafvbijlemf1  47389  fargshiftfva  47428  ichreuopeq  47458  2exopprim  47510  reuopreuprim  47511  fmtnoprmfac1  47550  proththd  47599  opoeALTV  47668  evensumeven  47692  sbgoldbalt  47766  evengpop3  47783  evengpoap3  47784  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  wtgoldbnnsum4prm  47787  bgoldbnnsum3prm  47789  tgoldbach  47802  dfclnbgr6  47841  dfsclnbgr6  47843  uhgrimedg  47876  uhgrimprop  47877  isuspgrimlem  47880  isuspgrim  47881  gricushgr  47902  uhgrimisgrgric  47916  isubgr3stgrlem7  47957  uspgrlimlem2  47974  gpgedgel  48035  gpgprismgriedgdmss  48037  gpgedgvtx0  48046  gpgedgiov  48050  gpgedg2ov  48051  gpgedg2iv  48052  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem3  48058  gpg5nbgrvtx03star  48065  gpg5nbgr3star  48066  gpg5gricstgr3  48075  pgnbgreunbgrlem4  48104  assintop  48194  uzlidlring  48220  2zrngnmrid  48241  cznrng  48246  lmodvsmdi  48364  lincsum  48415  lincsumcl  48417  el0ldep  48452  ldepspr  48459  lindssnlvec  48472  nn0digval  48586  1arympt1fv  48625  eenglngeehlnmlem1  48723  rrx2linest  48728  line2  48738  itsclc0yqe  48747  r19.41dv  48787  setrec1lem3  49675  aacllem  49787