Theorem anim1i 616

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 614	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  681  sylanr1  683  eu6im  2576  r19.28v  3169  rmob  3829  eqeuel  4306  preq12nebg  4807  fores  6756  fdmeu  6890  ssimaex  6919  dffv2  6929  exfo  7051  fpropnf1  7215  f1ocoima  7251  oprabv  7420  ndmovass  7548  fun11uni  7877  resf1ext2b  7879  fabexgOLD  7883  f1oabexgOLD  7887  f1iun  7890  soxp  8072  tz7.48lem  8373  tz7.49c  8378  omass  8508  oewordri  8521  omabs  8580  sbthlem9  9026  pssnn  9096  fineqvlem  9169  domunfican  9225  fiint  9230  fsuppsssupp  9287  sup0  9373  inf1  9534  infeq5  9549  cantnfle  9583  rankuni  9778  djuunxp  9836  acndom  9964  acnnum  9965  cdainflem  10101  cfcof  10187  ac6num  10392  ac6s2  10399  brdom5  10442  brdom4  10443  genpnnp  10919  divmulasscom  11824  lediv2a  12041  supmul1  12116  infregelb  12131  nn2ge  12195  btwnz  12623  eluz2b2  12862  uz2mulcl  12867  eqreznegel  12875  xrsupexmnf  13248  xrinfmexpnf  13249  xrsupsslem  13250  xrinfmsslem  13251  supxrun  13259  ioo0  13314  elioo4g  13350  fz0fzelfz0  13579  fz0fzdiffz0  13582  2ffzeq  13594  elfzodifsumelfzo  13677  elfzom1elp1fzo  13678  zpnn0elfzo  13684  elfzom1elp1fzo1  13713  fzonfzoufzol  13717  quoremnn0  13806  zmodidfzoimp  13851  modabs  13854  modaddb  13859  modifeq2int  13886  modaddmulmod  13891  expcl2lem  14026  hashgt23el  14377  hashreshashfun  14392  iswrdsymb  14484  ccatcl  14527  ccatsymb  14536  swrdfv2  14615  swrdsbslen  14618  swrdspsleq  14619  pfxswrd  14659  pfxccatin12lem3  14685  pfxccatpfx2  14690  swrdccat3blem  14692  reuccatpfxs1  14700  repswccat  14739  cshweqdifid  14773  lswco  14792  repsco  14793  s4f1o  14871  trclun  14967  mulre  15074  rediv  15084  imdiv  15091  resqrex  15203  caurcvg2  15631  fsumdifsnconst  15745  modfsummods  15747  tanval  16086  p1modz1  16219  negdvdsb  16232  muldvds1  16240  muldvds2  16241  dvdscmulr  16244  dvdsmulcr  16245  sumodd  16348  divalglem8  16360  divgcdnn  16475  lcmfunsnlem2lem2  16599  lcmfun  16605  2mulprm  16653  maxprmfct  16670  vfermltlALT  16764  modprm0  16767  pcpremul  16805  pcmul  16813  oddprmdvds  16865  prmdvdsprmo  17004  cshwsidrepsw  17055  gsumccat  18800  grpissubg  19113  ecqusaddd  19158  ecqusaddcl  19159  eqg0subg  19162  gim0to0  19235  gsmsymgreqlem2  19397  symgfixfo  19405  fsfnn0gsumfsffz  19949  rnglz  20137  isringrng  20259  irredn0  20394  c0snmgmhm  20433  rimisrngim  20466  zrrnghm  20504  rnghmsubcsetclem2  20600  rhmsubcsetclem2  20629  rhmsubcrngclem2  20635  lsppratlem1  21137  qusmulrng  21272  quscrng  21273  rngqiprngghmlem3  21279  rngqiprnglinlem3  21283  rngqiprngimf1lem  21284  rngqiprnglin  21292  cnfldfunALT  21359  cnfldfunALTOLD  21372  dvdsrzring  21451  mpofrlmd  21767  matinvgcell  22410  mat1dimcrng  22452  dmatscmcl  22478  scmatscm  22488  scmatghm  22508  scmatmhm  22509  ma1repvcl  22545  slesolinv  22655  slesolinvbi  22656  cramerimplem1  22658  cramerimp  22661  cramerlem1  22662  cramer  22666  cpmatacl  22691  cpmatmcl  22694  mat2pmatghm  22705  mat2pmatmul  22706  m2pmfzgsumcl  22723  decpmatmul  22747  decpmatmulsumfsupp  22748  pmatcollpwfi  22757  pm2mpf1  22774  pm2mpghm  22791  pm2mpmhmlem1  22793  monmat2matmon  22799  chpdmatlem2  22814  chpdmat  22816  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  clscld  23022  neiptopnei  23107  2ndcdisj2  23432  comppfsc  23507  tx1stc  23625  opnfbas  23817  fbasfip  23843  alexsublem  24019  alexsubALTlem4  24025  cnextcn  24042  ngpocelbl  24679  cphipval  25220  bcthlem5  25305  vitalilem4  25588  vitalilem5  25589  itg2mulc  25724  bddiblnc  25819  dvcobr  25923  dvcnvlem  25953  dvferm1  25962  dvne0  25988  mdegmullem  26053  plyeq0lem  26185  plyexmo  26290  aalioulem5  26313  aalioulem6  26314  aaliou  26315  cxple2a  26676  cxpaddlelem  26728  cxpaddle  26729  relogbcxpb  26764  bcmono  27254  lgsprme0  27316  gausslemma2dlem0e  27337  gausslemma2dlem1a  27342  gausslemma2dlem6  27349  lgsquadlem2  27358  2lgsoddprm  27393  elno2  27632  cofcutr  27930  colinearalg  28993  axcontlem3  29049  umgrislfupgrlem  29205  edgupgr  29217  usgruspgrb  29266  usgrislfuspgr  29270  edgssv2  29281  umgr2edg  29292  uspgredg2v  29307  usgrexmplef  29342  subupgr  29370  subusgr  29372  nbupgrres  29447  nb3gr2nb  29467  nbupgruvtxres  29490  cusgrres  29532  cusgrsizeindslem  29535  cusgrsizeinds  29536  vtxdun  29565  finrusgrfusgr  29649  cusgrrusgr  29665  pthdifv  29813  spthdep  29817  cycliscrct  29882  crctcshwlkn0lem6  29898  crctcshwlkn0lem7  29899  crctcshtrl  29906  crctcsh  29907  umgr2adedgwlkonALT  30030  elwwlks2  30052  elwspths2spth  30053  rusgrnumwwlk  30061  clwlkclwwlklem2a  30083  clwlkclwwlklem3  30086  clwwisshclwws  30100  wwlksubclwwlk  30143  eleclclwwlknlem2  30146  eupth2lem3lem3  30315  eucrct2eupth1  30329  frgr3v  30360  3vfriswmgr  30363  1to3vfriswmgr  30365  3cyclfrgr  30373  vdgn1frgrv2  30381  frgrwopreglem5  30406  frgrwopreglem5ALT  30407  frrusgrord0lem  30424  frrusgrord0  30425  2clwwlk2clwwlk  30435  extwwlkfab  30437  numclwwlk1lem2fo  30443  friendshipgt3  30483  ex-natded9.20-2  30503  grpoidinvlem3  30592  grpoidinv  30594  nmobndseqi  30865  nmobndseqiALT  30866  hvaddsub4  31164  ocsh  31369  5oalem2  31741  5oalem5  31744  3oalem2  31749  pjjsi  31786  hoadddir  31890  leopmul  32220  stge1i  32324  hatomistici  32448  mdsymlem2  32490  mdsymlem5  32493  addltmulALT  32532  isoun  32790  fsumiunle  32917  lsmsnorb  33466  crefdf  34008  qqhre  34180  esumiun  34254  sxbrsigalem0  34431  dya2iocnei  34442  sxbrsigalem5  34448  sibfinima  34499  eulerpartlemgs2  34540  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemsup  34665  bnj529  34900  bnj945  34932  bnj1098  34942  bnj1533  35010  bnj605  35065  bnj594  35070  bnj607  35074  bnj966  35102  bnj967  35103  bnj996  35114  bnj999  35116  bnj1006  35118  bnj1118  35142  bnj1172  35159  bnj1279  35176  bnj1296  35179  bnj1498  35219  fnrelpredd  35250  lfuhgr3  35318  loop1cycl  35335  cvmsi  35463  satf0op  35575  satffunlem1lem1  35600  satffunlem2lem1  35602  fv2ndcnv  35976  trisegint  36226  funtransport  36229  btwnconn1lem4  36288  btwnconn2  36300  segcon2  36303  outsideofeu  36329  isfne  36537  lukshef-ax2  36613  limsucncmpi  36643  weiunso  36664  bj-nsnid  37393  bj-restn0b  37419  bj-eldiag2  37507  bj-isrvec2  37630  pibt2  37747  unccur  37938  lindsadd  37948  lindsenlbs  37950  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem26  37981  poimirlem27  37982  poimirlem29  37984  poimirlem30  37985  poimirlem32  37987  heicant  37990  ismblfin  37996  itg2gt0cn  38010  areacirc  38048  opelopab3  38053  isdivrngo  38285  isdrngo2  38293  fldcrngo  38339  flddmn  38393  refrelredund4  39054  mainer2  39295  cmtbr4N  39715  linepsubN  40212  pmapsub  40228  paddasslem14  40293  pclcmpatN  40361  trlval2  40623  cdleme20  40784  cdleme21j  40796  dvalveclem  41485  dia2dimlem7  41530  dvhlveclem  41568  docaclN  41584  dihjat1  41889  mapdhcl  42187  mapdh6dN  42199  mapdh8  42248  hdmap1l6d  42273  hdmap10  42300  hdmaprnlem17N  42323  hdmaplkr  42373  hdmapip0  42375  hgmapvv  42386  aks6d1c4  42577  cmpfiiin  43143  pellexlem4  43278  pellqrex  43325  acongtr  43424  acongrep  43426  jm2.23  43442  omlimcl2  43688  onsucf1lem  43715  oege1  43752  nnoeomeqom  43758  cantnfresb  43770  onmcl  43777  tfsconcat0i  43791  ofoafg  43800  ofoafo  43802  ofoaass  43806  ofoacom  43807  naddcnfass  43815  rp-fakeanorass  43958  rp-isfinite6  43963  harval3  43983  inintabss  44023  rfovcnvf1od  44449  clsk1indlem3  44488  ntrclsk13  44516  pm10.55  44814  refsum2cnlem1  45486  axccd2  45677  mptssid  45688  fmuldfeq  46031  climsuse  46056  limclner  46097  climxlim2lem  46291  icccncfext  46333  stoweidlem26  46472  stoweidlem52  46498  stoweidlem57  46503  fourierdlem20  46573  fourierdlem41  46594  fourierdlem52  46604  fourierdlem64  46616  fourierdlem102  46654  fourierdlem114  46666  ovolval4lem1  47095  preimagelt  47145  preimalegt  47146  squeezedltsq  47334  funressneu  47507  afvelrn  47628  elfz2z  47775  2ffzoeq  47788  zplusmodne  47809  addmodne  47810  minusmod5ne  47815  modn0mul  47823  m1modmmod  47824  nndivides2  47844  imasetpreimafvbijlemfv  47874  imasetpreimafvbijlemf1  47876  fargshiftfva  47915  ichreuopeq  47945  2exopprim  47997  reuopreuprim  47998  fmtnoprmfac1  48040  proththd  48089  opoeALTV  48171  evensumeven  48195  sbgoldbalt  48269  evengpop3  48286  evengpoap3  48287  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  tgoldbach  48305  dfclnbgr6  48344  dfsclnbgr6  48346  uhgrimedg  48379  uhgrimprop  48380  isuspgrimlem  48383  isuspgrim  48384  gricushgr  48405  uhgrimisgrgric  48419  isubgr3stgrlem7  48460  uspgrlimlem2  48477  gpgedgel  48538  gpgprismgriedgdmss  48540  gpgedgvtx0  48549  gpgedgiov  48553  gpgedg2ov  48554  gpgedg2iv  48555  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem3  48561  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  gpg5gricstgr3  48578  pgnbgreunbgrlem4  48607  assintop  48697  uzlidlring  48723  2zrngnmrid  48744  cznrng  48749  lmodvsmdi  48867  lincsum  48917  lincsumcl  48919  el0ldep  48954  ldepspr  48961  lindssnlvec  48974  nn0digval  49088  1arympt1fv  49127  eenglngeehlnmlem1  49225  rrx2linest  49230  line2  49240  itsclc0yqe  49249  r19.41dv  49289  setrec1lem3  50176  aacllem  50288