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 396

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 206  df-an 397

This theorem is referenced by:  sylanl1  677  sylanr1  679  eu6im  2576  r19.28v  3117  rmob  3824  eqeuel  4297  preq12nebg  4794  fores  6707  ssimaex  6862  dffv2  6872  exfo  6990  fpropnf1  7149  oprabv  7344  ndmovass  7469  fun11uni  7788  fabexg  7790  f1oabexg  7792  f1iun  7795  soxp  7979  tz7.48lem  8281  tz7.49c  8286  omass  8420  oewordri  8432  omabs  8490  sbthlem9  8887  pssnn  8960  fineqvlem  9046  pssnnOLD  9049  domunfican  9096  fiint  9100  fsuppsssupp  9153  sup0  9234  inf1  9389  infeq5  9404  cantnfle  9438  rankuni  9630  djuunxp  9688  acndom  9816  acnnum  9817  cdainflem  9952  cfcof  10039  ac6num  10244  ac6s2  10251  brdom5  10294  brdom4  10295  genpnnp  10770  divmulasscom  11666  lediv2a  11878  supmul1  11953  infregelb  11968  nn2ge  12009  btwnz  12432  eluz2b2  12670  uz2mulcl  12675  eqreznegel  12683  xrsupexmnf  13048  xrinfmexpnf  13049  xrsupsslem  13050  xrinfmsslem  13051  supxrun  13059  ioo0  13113  elioo4g  13148  fz0fzelfz0  13371  fz0fzdiffz0  13374  2ffzeq  13386  elfzodifsumelfzo  13462  elfzom1elp1fzo  13463  zpnn0elfzo  13469  elfzom1elp1fzo1  13496  fzonfzoufzol  13499  quoremnn0  13585  zmodidfzoimp  13630  modabs  13633  modmuladd  13642  modifeq2int  13662  modaddmulmod  13667  expcl2lem  13803  hashgt23el  14148  hashreshashfun  14163  iswrdsymb  14243  ccatcl  14286  ccatsymb  14296  swrdfv2  14383  swrdsbslen  14386  swrdspsleq  14387  pfxswrd  14428  pfxccatin12lem3  14454  pfxccatpfx2  14459  swrdccat3blem  14461  reuccatpfxs1  14469  repswccat  14508  cshweqdifid  14542  lswco  14561  repsco  14562  s4f1o  14640  ccat2s1fvwALTOLD  14679  trclun  14734  mulre  14841  rediv  14851  imdiv  14858  resqrex  14971  caurcvg2  15398  fsumdifsnconst  15512  modfsummods  15514  tanval  15846  p1modz1  15979  negdvdsb  15991  muldvds1  15999  muldvds2  16000  dvdscmulr  16003  dvdsmulcr  16004  sumodd  16106  divalglem8  16118  divgcdnn  16231  lcmfunsnlem2lem2  16353  lcmfun  16359  2mulprm  16407  maxprmfct  16423  vfermltlALT  16512  modprm0  16515  pcpremul  16553  pcmul  16561  oddprmdvds  16613  prmdvdsprmo  16752  cshwsidrepsw  16804  gsumccat  18489  grpissubg  18784  gsmsymgreqlem2  19048  symgfixfo  19056  fsfnn0gsumfsffz  19593  irredn0  19954  gim0to0  19995  lsppratlem1  20418  cnfldfunALT  20619  dvdsrzring  20692  mpofrlmd  20993  matinvgcell  21593  mat1dimcrng  21635  dmatscmcl  21661  scmatscm  21671  scmatghm  21691  scmatmhm  21692  ma1repvcl  21728  slesolinv  21838  slesolinvbi  21839  cramerimplem1  21841  cramerimp  21844  cramerlem1  21845  cramer  21849  cpmatacl  21874  cpmatmcl  21877  mat2pmatghm  21888  mat2pmatmul  21889  m2pmfzgsumcl  21906  decpmatmul  21930  decpmatmulsumfsupp  21931  pmatcollpwfi  21940  pm2mpf1  21957  pm2mpghm  21974  pm2mpmhmlem1  21976  monmat2matmon  21982  chpdmatlem2  21997  chpdmat  21999  cpmadugsumlemB  22032  cpmadugsumlemC  22033  cpmadugsumlemF  22034  clscld  22207  neiptopnei  22292  2ndcdisj2  22617  comppfsc  22692  tx1stc  22810  opnfbas  23002  fbasfip  23028  alexsublem  23204  alexsubALTlem4  23210  cnextcn  23227  ngpocelbl  23877  cphipval  24416  bcthlem5  24501  vitalilem4  24784  vitalilem5  24785  itg2mulc  24921  bddiblnc  25015  dvcobr  25119  dvcnvlem  25149  dvferm1  25158  dvne0  25184  mdegmullem  25252  plyeq0lem  25380  plyexmo  25482  aalioulem5  25505  aalioulem6  25506  aaliou  25507  cxple2a  25863  cxpaddlelem  25913  cxpaddle  25914  relogbcxpb  25946  bcmono  26434  lgsprme0  26496  gausslemma2dlem0e  26517  gausslemma2dlem1a  26522  gausslemma2dlem6  26529  lgsquadlem2  26538  2lgsoddprm  26573  colinearalg  27287  axcontlem3  27343  umgrislfupgrlem  27501  edgupgr  27513  usgruspgrb  27560  usgrislfuspgr  27563  edgssv2  27574  umgr2edg  27585  uspgredg2v  27600  usgrexmplef  27635  subupgr  27663  subusgr  27665  nbupgrres  27740  nb3gr2nb  27760  nbupgruvtxres  27783  cusgrres  27824  cusgrsizeindslem  27827  cusgrsizeinds  27828  vtxdun  27857  finrusgrfusgr  27941  cusgrrusgr  27957  spthdep  28111  cycliscrct  28176  crctcshwlkn0lem6  28189  crctcshwlkn0lem7  28190  crctcshtrl  28197  crctcsh  28198  umgr2adedgwlkonALT  28321  elwwlks2  28340  elwspths2spth  28341  rusgrnumwwlk  28349  clwlkclwwlklem2a  28371  clwlkclwwlklem3  28374  clwwisshclwws  28388  wwlksubclwwlk  28431  eleclclwwlknlem2  28434  eupth2lem3lem3  28603  eucrct2eupth1  28617  frgr3v  28648  3vfriswmgr  28651  1to3vfriswmgr  28653  3cyclfrgr  28661  vdgn1frgrv2  28669  frgrwopreglem5  28694  frgrwopreglem5ALT  28695  frrusgrord0lem  28712  frrusgrord0  28713  2clwwlk2clwwlk  28723  extwwlkfab  28725  numclwwlk1lem2fo  28731  friendshipgt3  28771  ex-natded9.20-2  28791  grpoidinvlem3  28877  grpoidinv  28879  nmobndseqi  29150  nmobndseqiALT  29151  hvaddsub4  29449  ocsh  29654  5oalem2  30026  5oalem5  30029  3oalem2  30034  pjjsi  30071  hoadddir  30175  leopmul  30505  stge1i  30609  hatomistici  30733  mdsymlem2  30775  mdsymlem5  30778  addltmulALT  30817  isoun  31043  fsumiunle  31152  lsmsnorb  31588  crefdf  31807  qqhre  31979  esumiun  32071  sxbrsigalem0  32247  dya2iocnei  32258  sxbrsigalem5  32264  sibfinima  32315  eulerpartlemgs2  32356  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemsup  32480  bnj529  32730  bnj945  32762  bnj1098  32772  bnj1533  32841  bnj605  32896  bnj594  32901  bnj607  32905  bnj966  32933  bnj967  32934  bnj996  32945  bnj999  32947  bnj1006  32949  bnj1118  32973  bnj1172  32990  bnj1279  33007  bnj1296  33010  bnj1498  33050  fnrelpredd  33070  lfuhgr3  33090  loop1cycl  33108  cvmsi  33236  satf0op  33348  satffunlem1lem1  33373  satffunlem2lem1  33375  fv2ndcnv  33761  elno2  33866  cofcutr  34101  trisegint  34339  funtransport  34342  btwnconn1lem4  34401  btwnconn2  34413  segcon2  34416  outsideofeu  34442  isfne  34537  lukshef-ax2  34613  limsucncmpi  34643  bj-nsnid  35250  bj-restn0b  35271  bj-eldiag2  35357  bj-isrvec2  35480  pibt2  35597  unccur  35769  lindsadd  35779  lindsenlbs  35781  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem26  35812  poimirlem27  35813  poimirlem29  35815  poimirlem30  35816  poimirlem32  35818  heicant  35821  ismblfin  35827  itg2gt0cn  35841  areacirc  35879  opelopab3  35884  isdivrngo  36117  isdrngo2  36125  fldcrng  36171  flddmn  36225  refrelredund4  36755  cmtbr4N  37276  linepsubN  37773  pmapsub  37789  paddasslem14  37854  pclcmpatN  37922  trlval2  38184  cdleme20  38345  cdleme21j  38357  dvalveclem  39046  dia2dimlem7  39091  dvhlveclem  39129  docaclN  39145  dihjat1  39450  mapdhcl  39748  mapdh6dN  39760  mapdh8  39809  hdmap1l6d  39834  hdmap10  39861  hdmaprnlem17N  39884  hdmaplkr  39934  hdmapip0  39936  hgmapvv  39947  cmpfiiin  40526  pellexlem4  40661  pellqrex  40708  acongtr  40807  acongrep  40809  jm2.23  40825  rp-fakeanorass  41127  rp-isfinite6  41132  harval3  41152  inintabss  41193  rfovcnvf1od  41619  clsk1indlem3  41660  ntrclsk13  41688  pm10.55  41994  refsum2cnlem1  42587  axccd2  42776  mptssid  42792  fmuldfeq  43131  climsuse  43156  limclner  43199  climxlim2lem  43393  icccncfext  43435  stoweidlem26  43574  stoweidlem52  43600  stoweidlem57  43605  fourierdlem20  43675  fourierdlem41  43696  fourierdlem52  43706  fourierdlem64  43718  fourierdlem102  43756  fourierdlem114  43768  ovolval4lem1  44194  preimagelt  44244  preimalegt  44245  funressneu  44552  afvelrn  44671  elfz2z  44818  2ffzoeq  44831  imasetpreimafvbijlemfv  44865  imasetpreimafvbijlemf1  44867  fargshiftfva  44906  ichreuopeq  44936  2exopprim  44988  reuopreuprim  44989  fmtnoprmfac1  45028  proththd  45077  opoeALTV  45146  evensumeven  45170  sbgoldbalt  45244  evengpop3  45261  evengpoap3  45262  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  tgoldbach  45280  isomushgr  45289  assintop  45414  isringrng  45450  rnglz  45453  c0snmgmhm  45483  zrrnghm  45486  uzlidlring  45498  2zrngnmrid  45519  cznrng  45524  rnghmsubcsetclem2  45545  rhmsubcsetclem2  45591  rhmsubcrngclem2  45597  lmodvsmdi  45729  lincsum  45781  lincsumcl  45783  el0ldep  45818  ldepspr  45825  lindssnlvec  45838  modn0mul  45877  m1modmmod  45878  nn0digval  45957  1arympt1fv  45996  eenglngeehlnmlem1  46094  rrx2linest  46099  line2  46109  itsclc0yqe  46118  r19.41dv  46158  setrec1lem3  46406  aacllem  46516