Theorem anim1i 627

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 23	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	anim12i 625	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylanl1  693  sylanr1  695  ax12ev2c  2216  eu6im  2600  r19.28v  3193  rmob  3836  eqeuel  4312  preq12nebg  4822  fores  6806  fdmeu  6941  ssimaex  6970  dffv2  6980  exfo  7105  fpropnf1  7271  f1ocoima  7311  oprabv  7480  ndmovass  7609  fun11uni  7945  resf1ext2b  7947  f1iun  7956  soxp  8141  tz7.48lemOLD  8451  tz7.49c  8456  omass  8588  oewordri  8601  omabs  8660  sbthlem9  9114  pssnn  9184  fineqvlem  9257  domunfican  9313  fiint  9318  fsuppsssupp  9373  sup0  9459  inf1  9623  infeq5  9638  cantnfle  9672  rankuni  9879  setrec1lem3  9969  djuunxp  10002  acndom  10130  acnnum  10131  cdainflem  10266  cfcof  10352  ac6num  10557  ac6s2  10564  brdom5  10608  brdom4  10609  genpnnp  11090  divmulasscom  11998  lediv2a  12211  supmul1  12286  infregelb  12301  nn2ge  12365  btwnz  12802  eluz2b2  13048  uz2mulcl  13053  eqreznegel  13061  xrsupexmnf  13435  xrinfmexpnf  13436  xrsupsslem  13437  xrinfmsslem  13438  supxrun  13446  ioo0  13501  elioo4g  13537  fz0fzelfz0  13768  fz0fzdiffz0  13771  2ffzeq  13783  elfzodifsumelfzo  13866  elfzom1elp1fzo  13867  zpnn0elfzo  13873  elfzom1elp1fzo1  13902  fzonfzoufzol  13906  quoremnn0  13996  zmodidfzoimp  14041  modabs  14044  modaddb  14049  modifeq2int  14076  modaddmulmod  14081  expcl2lem  14216  hashgt23el  14569  hashreshashfun  14584  iswrdsymb  14676  ccatcl  14719  ccatsymb  14728  swrdfv2  14811  swrdsbslen  14814  swrdspsleq  14815  pfxswrd  14855  pfxccatin12lem3  14881  pfxccatpfx2  14886  swrdccat3blem  14888  reuccatpfxs1  14896  repswccat  14937  cshweqdifid  14971  lswco  14990  repsco  14991  s4f1o  15069  trclun  15167  mulre  15288  rediv  15298  imdiv  15305  resqrex  15417  caurcvg2  15845  fsumdifsnconst  15958  modfsummods  15960  tanval  16296  p1modz1  16429  negdvdsb  16442  muldvds1  16450  muldvds2  16451  dvdscmulr  16454  dvdsmulcr  16455  sumodd  16558  divalglem8  16570  divgcdnn  16687  lcmfunsnlem2lem2  16814  lcmfun  16820  2mulprm  16868  maxprmfct  16885  vfermltlALT  16980  modprm0  16983  pcpremul  17021  pcmul  17029  oddprmdvds  17081  prmdvdsprmo  17220  cshwsidrepsw  17271  gsumccat  19037  grpissubg  19357  ecqusaddd  19407  ecqusaddcl  19408  eqg0subg  19411  gim0to0  19483  gsmsymgreqlem2  19645  symgfixfo  19653  fsfnn0gsumfsffz  20197  rnglz  20387  isringrng  20516  irredn0  20653  c0snmgmhm  20692  rimisrngim  20735  zrrnghm  20788  rnghmsubcsetclem2  20884  rhmsubcsetclem2  20913  rhmsubcrngclem2  20919  lsppratlem1  21425  qusmulrng  21578  quscrng  21579  rngqiprngghmlem3  21585  rngqiprnglinlem3  21589  rngqiprngimf1lem  21590  rngqiprnglin  21598  cnfldfunALT  21693  dvdsrzring  21767  mpofrlmd  22083  lindsenlbs  22157  matinvgcell  22750  mat1dimcrng  22792  dmatscmcl  22818  scmatscm  22828  scmatghm  22848  scmatmhm  22849  ma1repvcl  22885  matunitlindflem1  22994  matunitlindflem2  22995  slesolinv  22998  slesolinvbi  22999  cramerimplem1  23001  cramerimp  23004  cramerlem1  23005  cramer  23009  cpmatacl  23034  cpmatmcl  23037  mat2pmatghm  23048  mat2pmatmul  23049  m2pmfzgsumcl  23066  decpmatmul  23090  decpmatmulsumfsupp  23091  pmatcollpwfi  23100  pm2mpf1  23117  pm2mpghm  23134  pm2mpmhmlem1  23136  monmat2matmon  23142  chpdmatlem2  23157  chpdmat  23159  cpmadugsumlemB  23192  cpmadugsumlemC  23193  cpmadugsumlemF  23194  clscld  23365  neiptopnei  23450  2ndcdisj2  23776  comppfsc  23851  tx1stc  23969  opnfbas  24161  fbasfip  24187  alexsublem  24363  alexsubALTlem4  24369  cnextcn  24386  ngpocelbl  25023  cphipval  25564  bcthlem5  25649  vitalilem4  25932  vitalilem5  25933  itg2mulc  26068  bddiblnc  26162  dvcobr  26266  dvcnvlem  26296  dvferm1  26305  dvne0  26331  mdegmullem  26396  plyeq0lem  26529  plyexmo  26636  aalioulem5  26663  aalioulem6  26664  aaliou  26665  cxple2a  27027  cxpaddlelem  27079  cxpaddle  27080  relogbcxpb  27115  bcmono  27604  lgsprme0  27666  gausslemma2dlem0e  27687  gausslemma2dlem1a  27692  gausslemma2dlem6  27699  lgsquadlem2  27708  2lgsoddprm  27743  fltoprmlem1  27993  elno2  28011  cofcutr  28310  colinearalg  29488  axcontlem3  29544  umgrislfupgrlem  29700  edgupgr  29712  lfuhgr3  29728  usgruspgrb  29764  usgrislfuspgr  29768  edgssv2  29779  umgr2edg  29790  uspgredg2v  29805  usgrexmplef  29840  subupgr  29868  subusgr  29870  nbupgrres  29945  nb3gr2nb  29965  nbupgruvtxres  29988  cusgrres  30029  cusgrsizeindslem  30032  cusgrsizeinds  30033  vtxdun  30062  finrusgrfusgr  30146  cusgrrusgr  30162  pthdifv  30316  spthdep  30320  cycliscrct  30387  crctcshwlkn0lem6  30404  crctcshwlkn0lem7  30405  crctcshtrl  30412  crctcsh  30413  umgr2adedgwlkonALT  30536  elwwlks2  30558  elwspths2spth  30559  rusgrnumwwlk  30567  clwlkclwwlklem2a  30589  clwlkclwwlklem3  30592  clwwisshclwws  30606  wwlksubclwwlk  30649  eleclclwwlknlem2  30652  loop1cycl  30744  eupth2lem3lem3  30831  eucrct2eupth1  30845  frgr3v  30876  3vfriswmgr  30879  1to3vfriswmgr  30881  3cyclfrgr  30889  vdgn1frgrv2  30897  frgrwopreglem5  30922  frgrwopreglem5ALT  30923  frrusgrord0lem  30940  frrusgrord0  30941  2clwwlk2clwwlk  30951  extwwlkfab  30953  numclwwlk1lem2fo  30959  friendshipgt3  30999  ex-natded9.20-2  31019  grpoidinvlem3  31108  grpoidinv  31110  nmobndseqi  31381  nmobndseqiALT  31382  hvaddsub4  31680  ocsh  31885  5oalem2  32257  5oalem5  32260  3oalem2  32265  pjjsi  32302  hoadddir  32406  leopmul  32736  stge1i  32840  hatomistici  32964  mdsymlem2  33006  mdsymlem5  33009  addltmulALT  33048  isoun  33295  fsumiunle  33420  lsmsnorb  33946  crefdf  34480  qqhre  34652  esumiun  34726  sxbrsigalem0  34903  dya2iocnei  34914  sxbrsigalem5  34920  sibfinima  34971  eulerpartlemgs2  35012  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemsup  35137  bnj529  35372  bnj945  35404  bnj1098  35414  bnj1533  35482  bnj605  35537  bnj594  35542  bnj607  35546  bnj966  35574  bnj967  35575  bnj996  35586  bnj999  35588  bnj1006  35590  bnj1118  35614  bnj1172  35631  bnj1279  35648  bnj1296  35651  bnj1498  35691  fnrelpredd  35720  cvmsi  36030  satf0op  36142  satffunlem1lem1  36167  satffunlem2lem1  36169  fv2ndcnv  36542  trisegint  36793  funtransport  36796  btwnconn1lem4  36855  btwnconn2  36867  segcon2  36870  outsideofeu  36896  isfne  37127  lukshef-ax2  37203  limsucncmpi  37233  weiunso  37254  bj-nsnid  37985  bj-restn0b  38012  bj-eldiag2  38099  bj-isrvec2  38222  pibt2  38341  unccur  38527  lindsadd  38537  poimirlem26  38565  poimirlem27  38566  poimirlem29  38568  poimirlem30  38569  poimirlem32  38571  heicant  38574  ismblfin  38580  itg2gt0cn  38594  areacirc  38632  impprop  38645  opelopab3  38653  isdivrngo  38885  isdrngo2  38893  fldcrngo  38939  flddmn  38993  refrelredund4  39652  mainer2  39893  cmtbr4N  40313  linepsubN  40810  pmapsub  40826  paddasslem14  40891  pclcmpatN  40959  trlval2  41221  cdleme20  41382  cdleme21j  41394  dvalveclem  42083  dia2dimlem7  42128  dvhlveclem  42166  docaclN  42182  dihjat1  42487  mapdhcl  42785  mapdh6dN  42797  mapdh8  42846  hdmap1l6d  42871  hdmap10  42898  hdmaprnlem17N  42921  hdmaplkr  42971  hdmapip0  42973  hgmapvv  42984  aks6d1c4  43175  cmpfiiin  43708  pellexlem4  43839  pellqrex  43886  acongtr  43985  acongrep  43987  jm2.23  44003  omlimcl2  44244  onsucf1lem  44271  oege1  44308  nnoeomeqom  44314  cantnfresb  44326  onmcl  44333  tfsconcat0i  44347  ofoafg  44356  ofoafo  44358  ofoaass  44362  ofoacom  44363  naddcnfass  44371  rp-fakeanorass  44514  rp-isfinite6  44519  harval3  44539  inintabss  44579  rfovcnvf1od  45004  clsk1indlem3  45043  ntrclsk13  45071  pm10.55  45353  refsum2cnlem1  46054  axccd2  46242  mptssid  46253  fmuldfeq  46595  climsuse  46620  limclner  46661  climxlim2lem  46855  icccncfext  46897  stoweidlem26  47036  stoweidlem52  47062  stoweidlem57  47067  fourierdlem20  47137  fourierdlem41  47158  fourierdlem52  47168  fourierdlem64  47180  fourierdlem102  47218  fourierdlem114  47230  ovolval4lem1  47659  preimagelt  47709  preimalegt  47710  squeezedltsq  47912  funressneu  48117  afvelrn  48238  elfz2z  48385  2ffzoeq  48398  zplusmodne  48419  addmodne  48420  minusmod5ne  48425  modn0mul  48433  m1modmmod  48434  nndivides2  48454  imasetpreimafvbijlemfv  48484  imasetpreimafvbijlemf1  48486  fargshiftfva  48525  ichreuopeq  48555  2exopprim  48607  reuopreuprim  48608  fmtnoprmfac1  48650  proththd  48699  opoeALTV  48781  evensumeven  48805  sbgoldbalt  48879  evengpop3  48896  evengpoap3  48897  nnsum4primeseven  48898  nnsum4primesevenALTV  48899  wtgoldbnnsum4prm  48900  bgoldbnnsum3prm  48902  tgoldbach  48915  dfclnbgr6  48954  dfsclnbgr6  48956  uhgrimedg  48989  uhgrimprop  48990  isuspgrimlem  48993  isuspgrim  48994  gricushgr  49015  uhgrimisgrgric  49029  isubgr3stgrlem7  49070  uspgrlimlem2  49087  gpgedgel  49148  gpgprismgriedgdmss  49150  gpgedgvtx0  49159  gpgedgiov  49163  gpgedg2ov  49164  gpgedg2iv  49165  gpg5nbgrvtx03starlem2  49167  gpg5nbgrvtx13starlem1  49169  gpg5nbgrvtx13starlem3  49171  gpg5nbgrvtx03star  49178  gpg5nbgr3star  49179  gpg5gricstgr3  49188  pgnbgreunbgrlem4  49217  assintop  49306  uzlidlring  49332  2zrngnmrid  49353  cznrng  49358  lmodvsmdi  49491  lincsum  49541  lincsumcl  49543  el0ldep  49578  ldepspr  49585  lindssnlvec  49598  nn0digval  49712  1arympt1fv  49751  eenglngeehlnmlem1  49849  rrx2linest  49854  line2  49864  itsclc0yqe  49873  r19.41dv  49912  aacllem  50939