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  2574  r19.28v  3175  rmob  3865  eqeuel  4340  preq12nebg  4839  fores  6799  fdmeu  6934  ssimaex  6963  dffv2  6973  exfo  7094  fpropnf1  7259  f1ocoima  7295  oprabv  7465  ndmovass  7593  fun11uni  7927  resf1ext2b  7929  fabexgOLD  7933  f1oabexgOLD  7937  f1iun  7940  soxp  8126  tz7.48lem  8453  tz7.49c  8458  omass  8590  oewordri  8602  omabs  8661  sbthlem9  9103  pssnn  9180  fineqvlem  9268  domunfican  9331  fiint  9336  fiintOLD  9337  fsuppsssupp  9391  sup0  9477  inf1  9634  infeq5  9649  cantnfle  9683  rankuni  9875  djuunxp  9933  acndom  10063  acnnum  10064  cdainflem  10200  cfcof  10286  ac6num  10491  ac6s2  10498  brdom5  10541  brdom4  10542  genpnnp  11017  divmulasscom  11918  lediv2a  12134  supmul1  12209  infregelb  12224  nn2ge  12265  btwnz  12694  eluz2b2  12935  uz2mulcl  12940  eqreznegel  12948  xrsupexmnf  13319  xrinfmexpnf  13320  xrsupsslem  13321  xrinfmsslem  13322  supxrun  13330  ioo0  13385  elioo4g  13421  fz0fzelfz0  13649  fz0fzdiffz0  13652  2ffzeq  13664  elfzodifsumelfzo  13745  elfzom1elp1fzo  13746  zpnn0elfzo  13752  elfzom1elp1fzo1  13781  fzonfzoufzol  13784  quoremnn0  13871  zmodidfzoimp  13916  modabs  13919  modifeq2int  13949  modaddmulmod  13954  expcl2lem  14089  hashgt23el  14440  hashreshashfun  14455  iswrdsymb  14547  ccatcl  14590  ccatsymb  14598  swrdfv2  14677  swrdsbslen  14680  swrdspsleq  14681  pfxswrd  14722  pfxccatin12lem3  14748  pfxccatpfx2  14753  swrdccat3blem  14755  reuccatpfxs1  14763  repswccat  14802  cshweqdifid  14836  lswco  14856  repsco  14857  s4f1o  14935  trclun  15031  mulre  15138  rediv  15148  imdiv  15155  resqrex  15267  caurcvg2  15692  fsumdifsnconst  15805  modfsummods  15807  tanval  16144  p1modz1  16277  negdvdsb  16290  muldvds1  16298  muldvds2  16299  dvdscmulr  16302  dvdsmulcr  16303  sumodd  16405  divalglem8  16417  divgcdnn  16532  lcmfunsnlem2lem2  16656  lcmfun  16662  2mulprm  16710  maxprmfct  16726  vfermltlALT  16820  modprm0  16823  pcpremul  16861  pcmul  16869  oddprmdvds  16921  prmdvdsprmo  17060  cshwsidrepsw  17111  gsumccat  18817  grpissubg  19127  ecqusaddd  19173  ecqusaddcl  19174  eqg0subg  19177  gim0to0  19250  gsmsymgreqlem2  19410  symgfixfo  19418  fsfnn0gsumfsffz  19962  rnglz  20123  isringrng  20245  irredn0  20381  c0snmgmhm  20420  rimisrngim  20456  zrrnghm  20494  rnghmsubcsetclem2  20590  rhmsubcsetclem2  20619  rhmsubcrngclem2  20625  lsppratlem1  21106  qusmulrng  21241  quscrng  21242  rngqiprngghmlem3  21248  rngqiprnglinlem3  21252  rngqiprngimf1lem  21253  rngqiprnglin  21261  cnfldfunALT  21328  cnfldfunALTOLD  21341  dvdsrzring  21420  mpofrlmd  21735  matinvgcell  22371  mat1dimcrng  22413  dmatscmcl  22439  scmatscm  22449  scmatghm  22469  scmatmhm  22470  ma1repvcl  22506  slesolinv  22616  slesolinvbi  22617  cramerimplem1  22619  cramerimp  22622  cramerlem1  22623  cramer  22627  cpmatacl  22652  cpmatmcl  22655  mat2pmatghm  22666  mat2pmatmul  22667  m2pmfzgsumcl  22684  decpmatmul  22708  decpmatmulsumfsupp  22709  pmatcollpwfi  22718  pm2mpf1  22735  pm2mpghm  22752  pm2mpmhmlem1  22754  monmat2matmon  22760  chpdmatlem2  22775  chpdmat  22777  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  clscld  22983  neiptopnei  23068  2ndcdisj2  23393  comppfsc  23468  tx1stc  23586  opnfbas  23778  fbasfip  23804  alexsublem  23980  alexsubALTlem4  23986  cnextcn  24003  ngpocelbl  24641  cphipval  25193  bcthlem5  25278  vitalilem4  25562  vitalilem5  25563  itg2mulc  25698  bddiblnc  25793  dvcobr  25899  dvcobrOLD  25900  dvcnvlem  25930  dvferm1  25939  dvne0  25966  mdegmullem  26033  plyeq0lem  26165  plyexmo  26271  aalioulem5  26294  aalioulem6  26295  aaliou  26296  cxple2a  26658  cxpaddlelem  26711  cxpaddle  26712  relogbcxpb  26747  bcmono  27238  lgsprme0  27300  gausslemma2dlem0e  27321  gausslemma2dlem1a  27326  gausslemma2dlem6  27333  lgsquadlem2  27342  2lgsoddprm  27377  elno2  27616  cofcutr  27875  colinearalg  28835  axcontlem3  28891  umgrislfupgrlem  29047  edgupgr  29059  usgruspgrb  29108  usgrislfuspgr  29112  edgssv2  29123  umgr2edg  29134  uspgredg2v  29149  usgrexmplef  29184  subupgr  29212  subusgr  29214  nbupgrres  29289  nb3gr2nb  29309  nbupgruvtxres  29332  cusgrres  29374  cusgrsizeindslem  29377  cusgrsizeinds  29378  vtxdun  29407  finrusgrfusgr  29491  cusgrrusgr  29507  pthdifv  29658  spthdep  29662  cycliscrct  29727  crctcshwlkn0lem6  29743  crctcshwlkn0lem7  29744  crctcshtrl  29751  crctcsh  29752  umgr2adedgwlkonALT  29875  elwwlks2  29894  elwspths2spth  29895  rusgrnumwwlk  29903  clwlkclwwlklem2a  29925  clwlkclwwlklem3  29928  clwwisshclwws  29942  wwlksubclwwlk  29985  eleclclwwlknlem2  29988  eupth2lem3lem3  30157  eucrct2eupth1  30171  frgr3v  30202  3vfriswmgr  30205  1to3vfriswmgr  30207  3cyclfrgr  30215  vdgn1frgrv2  30223  frgrwopreglem5  30248  frgrwopreglem5ALT  30249  frrusgrord0lem  30266  frrusgrord0  30267  2clwwlk2clwwlk  30277  extwwlkfab  30279  numclwwlk1lem2fo  30285  friendshipgt3  30325  ex-natded9.20-2  30345  grpoidinvlem3  30433  grpoidinv  30435  nmobndseqi  30706  nmobndseqiALT  30707  hvaddsub4  31005  ocsh  31210  5oalem2  31582  5oalem5  31585  3oalem2  31590  pjjsi  31627  hoadddir  31731  leopmul  32061  stge1i  32165  hatomistici  32289  mdsymlem2  32331  mdsymlem5  32334  addltmulALT  32373  isoun  32625  fsumiunle  32754  lsmsnorb  33352  crefdf  33825  qqhre  33997  esumiun  34071  sxbrsigalem0  34249  dya2iocnei  34260  sxbrsigalem5  34266  sibfinima  34317  eulerpartlemgs2  34358  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemsup  34483  bnj529  34718  bnj945  34750  bnj1098  34760  bnj1533  34829  bnj605  34884  bnj594  34889  bnj607  34893  bnj966  34921  bnj967  34922  bnj996  34933  bnj999  34935  bnj1006  34937  bnj1118  34961  bnj1172  34978  bnj1279  34995  bnj1296  34998  bnj1498  35038  fnrelpredd  35066  lfuhgr3  35088  loop1cycl  35105  cvmsi  35233  satf0op  35345  satffunlem1lem1  35370  satffunlem2lem1  35372  fv2ndcnv  35741  trisegint  35992  funtransport  35995  btwnconn1lem4  36054  btwnconn2  36066  segcon2  36069  outsideofeu  36095  isfne  36303  lukshef-ax2  36379  limsucncmpi  36409  weiunso  36430  bj-nsnid  37034  bj-restn0b  37055  bj-eldiag2  37141  bj-isrvec2  37264  pibt2  37381  unccur  37573  lindsadd  37583  lindsenlbs  37585  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem26  37616  poimirlem27  37617  poimirlem29  37619  poimirlem30  37620  poimirlem32  37622  heicant  37625  ismblfin  37631  itg2gt0cn  37645  areacirc  37683  opelopab3  37688  isdivrngo  37920  isdrngo2  37928  fldcrngo  37974  flddmn  38028  refrelredund4  38599  mainer2  38810  cmtbr4N  39219  linepsubN  39717  pmapsub  39733  paddasslem14  39798  pclcmpatN  39866  trlval2  40128  cdleme20  40289  cdleme21j  40301  dvalveclem  40990  dia2dimlem7  41035  dvhlveclem  41073  docaclN  41089  dihjat1  41394  mapdhcl  41692  mapdh6dN  41704  mapdh8  41753  hdmap1l6d  41778  hdmap10  41805  hdmaprnlem17N  41828  hdmaplkr  41878  hdmapip0  41880  hgmapvv  41891  aks6d1c4  42083  cmpfiiin  42667  pellexlem4  42802  pellqrex  42849  acongtr  42949  acongrep  42951  jm2.23  42967  omlimcl2  43213  onsucf1lem  43240  oege1  43277  nnoeomeqom  43283  cantnfresb  43295  onmcl  43302  tfsconcat0i  43316  ofoafg  43325  ofoafo  43327  ofoaass  43331  ofoacom  43332  naddcnfass  43340  rp-fakeanorass  43484  rp-isfinite6  43489  harval3  43509  inintabss  43549  rfovcnvf1od  43975  clsk1indlem3  44014  ntrclsk13  44042  pm10.55  44341  refsum2cnlem1  45009  axccd2  45202  mptssid  45213  fmuldfeq  45560  climsuse  45585  limclner  45628  climxlim2lem  45822  icccncfext  45864  stoweidlem26  46003  stoweidlem52  46029  stoweidlem57  46034  fourierdlem20  46104  fourierdlem41  46125  fourierdlem52  46135  fourierdlem64  46147  fourierdlem102  46185  fourierdlem114  46197  ovolval4lem1  46626  preimagelt  46676  preimalegt  46677  squeezedltsq  46866  funressneu  47024  afvelrn  47145  elfz2z  47292  2ffzoeq  47304  zplusmodne  47320  addmodne  47321  minusmod5ne  47326  imasetpreimafvbijlemfv  47364  imasetpreimafvbijlemf1  47366  fargshiftfva  47405  ichreuopeq  47435  2exopprim  47487  reuopreuprim  47488  fmtnoprmfac1  47527  proththd  47576  opoeALTV  47645  evensumeven  47669  sbgoldbalt  47743  evengpop3  47760  evengpoap3  47761  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  tgoldbach  47779  dfclnbgr6  47817  dfsclnbgr6  47819  uhgrimedg  47852  uhgrimprop  47853  isuspgrimlem  47856  isuspgrim  47857  gricushgr  47878  uhgrimisgrgric  47892  isubgr3stgrlem7  47932  uspgrlimlem2  47949  gpgedgel  48002  gpgprismgriedgdmss  48004  gpgedgvtx0  48013  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem3  48023  gpg5nbgrvtx03star  48030  gpg5nbgr3star  48031  gpg5gricstgr3  48040  assintop  48132  uzlidlring  48158  2zrngnmrid  48179  cznrng  48184  lmodvsmdi  48302  lincsum  48353  lincsumcl  48355  el0ldep  48390  ldepspr  48397  lindssnlvec  48410  modn0mul  48448  m1modmmod  48449  nn0digval  48528  1arympt1fv  48567  eenglngeehlnmlem1  48665  rrx2linest  48670  line2  48680  itsclc0yqe  48689  r19.41dv  48729  setrec1lem3  49501  aacllem  49613