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  4817  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  8143  tz7.48lemOLD  8454  tz7.49c  8459  omass  8591  oewordri  8604  omabs  8663  sbthlem9  9117  pssnn  9187  fineqvlem  9260  domunfican  9316  fiint  9321  fsuppsssupp  9376  sup0  9462  inf1  9626  infeq5  9641  cantnfle  9675  rankuni  9882  setrec1lem3  9972  djuunxp  10005  acndom  10133  acnnum  10134  cdainflem  10269  cfcof  10355  ac6num  10560  ac6s2  10567  brdom5  10611  brdom4  10612  genpnnp  11093  divmulasscom  12001  lediv2a  12214  supmul1  12289  infregelb  12304  nn2ge  12368  btwnz  12805  eluz2b2  13051  uz2mulcl  13056  eqreznegel  13064  xrsupexmnf  13438  xrinfmexpnf  13439  xrsupsslem  13440  xrinfmsslem  13441  supxrun  13449  ioo0  13504  elioo4g  13540  fz0fzelfz0  13771  fz0fzdiffz0  13774  2ffzeq  13786  elfzodifsumelfzo  13869  elfzom1elp1fzo  13870  zpnn0elfzo  13876  elfzom1elp1fzo1  13905  fzonfzoufzol  13909  quoremnn0  13999  zmodidfzoimp  14044  modabs  14047  modaddb  14052  modifeq2int  14079  modaddmulmod  14084  expcl2lem  14219  hashgt23el  14572  hashreshashfun  14587  iswrdsymb  14679  ccatcl  14722  ccatsymb  14731  swrdfv2  14815  swrdsbslen  14818  swrdspsleq  14819  pfxswrd  14859  pfxccatin12lem3  14885  pfxccatpfx2  14890  swrdccat3blem  14892  reuccatpfxs1  14900  repswccat  14941  cshweqdifid  14975  lswco  14994  repsco  14995  s4f1o  15074  trclun  15172  mulre  15293  rediv  15303  imdiv  15310  resqrex  15422  caurcvg2  15850  fsumdifsnconst  15963  modfsummods  15965  tanval  16301  p1modz1  16434  negdvdsb  16447  muldvds1  16455  muldvds2  16456  dvdscmulr  16459  dvdsmulcr  16460  sumodd  16563  divalglem8  16575  divgcdnn  16692  lcmfunsnlem2lem2  16819  lcmfun  16825  2mulprm  16873  maxprmfct  16890  vfermltlALT  16985  modprm0  16988  pcpremul  17026  pcmul  17034  oddprmdvds  17086  prmdvdsprmo  17225  cshwsidrepsw  17276  gsumccat  19042  grpissubg  19362  ecqusaddd  19412  ecqusaddcl  19413  eqg0subg  19416  gim0to0  19488  gsmsymgreqlem2  19650  symgfixfo  19658  fsfnn0gsumfsffz  20202  rnglz  20392  isringrng  20521  irredn0  20658  c0snmgmhm  20697  rimisrngim  20740  zrrnghm  20793  rnghmsubcsetclem2  20889  rhmsubcsetclem2  20918  rhmsubcrngclem2  20924  lsppratlem1  21430  qusmulrng  21583  quscrng  21584  rngqiprngghmlem3  21590  rngqiprnglinlem3  21594  rngqiprngimf1lem  21595  rngqiprnglin  21603  cnfldfunALT  21698  dvdsrzring  21772  mpofrlmd  22088  lindsenlbs  22162  matinvgcell  22755  mat1dimcrng  22797  dmatscmcl  22823  scmatscm  22833  scmatghm  22853  scmatmhm  22854  ma1repvcl  22890  matunitlindflem1  22999  matunitlindflem2  23000  slesolinv  23003  slesolinvbi  23004  cramerimplem1  23006  cramerimp  23009  cramerlem1  23010  cramer  23014  cpmatacl  23039  cpmatmcl  23042  mat2pmatghm  23053  mat2pmatmul  23054  m2pmfzgsumcl  23071  decpmatmul  23095  decpmatmulsumfsupp  23096  pmatcollpwfi  23105  pm2mpf1  23122  pm2mpghm  23139  pm2mpmhmlem1  23141  monmat2matmon  23147  chpdmatlem2  23162  chpdmat  23164  cpmadugsumlemB  23197  cpmadugsumlemC  23198  cpmadugsumlemF  23199  clscld  23370  neiptopnei  23455  2ndcdisj2  23781  comppfsc  23856  tx1stc  23974  opnfbas  24166  fbasfip  24192  alexsublem  24368  alexsubALTlem4  24374  cnextcn  24391  ngpocelbl  25028  cphipval  25569  bcthlem5  25654  vitalilem4  25937  vitalilem5  25938  itg2mulc  26073  bddiblnc  26167  dvcobr  26271  dvcnvlem  26301  dvferm1  26310  dvne0  26336  mdegmullem  26401  plyeq0lem  26534  plyexmo  26641  aalioulem5  26668  aalioulem6  26669  aaliou  26670  cxple2a  27032  cxpaddlelem  27084  cxpaddle  27085  relogbcxpb  27120  bcmono  27609  lgsprme0  27671  gausslemma2dlem0e  27692  gausslemma2dlem1a  27697  gausslemma2dlem6  27704  lgsquadlem2  27713  2lgsoddprm  27748  flt4lem2  27982  fltoprmlem1  27998  elno2  28016  cofcutr  28315  colinearalg  29493  axcontlem3  29549  umgrislfupgrlem  29705  edgupgr  29717  lfuhgr3  29733  usgruspgrb  29769  usgrislfuspgr  29773  edgssv2  29784  umgr2edg  29795  uspgredg2v  29810  usgrexmplef  29845  subupgr  29873  subusgr  29875  nbupgrres  29950  nb3gr2nb  29970  nbupgruvtxres  29993  cusgrres  30034  cusgrsizeindslem  30037  cusgrsizeinds  30038  vtxdun  30067  finrusgrfusgr  30151  cusgrrusgr  30167  pthdifv  30321  spthdep  30325  cycliscrct  30392  crctcshwlkn0lem6  30409  crctcshwlkn0lem7  30410  crctcshtrl  30417  crctcsh  30418  umgr2adedgwlkonALT  30541  elwwlks2  30563  elwspths2spth  30564  rusgrnumwwlk  30572  clwlkclwwlklem2a  30594  clwlkclwwlklem3  30597  clwwisshclwws  30611  wwlksubclwwlk  30654  eleclclwwlknlem2  30657  loop1cycl  30749  eupth2lem3lem3  30836  eucrct2eupth1  30850  frgr3v  30881  3vfriswmgr  30884  1to3vfriswmgr  30886  3cyclfrgr  30894  vdgn1frgrv2  30902  frgrwopreglem5  30927  frgrwopreglem5ALT  30928  frrusgrord0lem  30945  frrusgrord0  30946  2clwwlk2clwwlk  30956  extwwlkfab  30958  numclwwlk1lem2fo  30964  friendshipgt3  31004  ex-natded9.20-2  31024  grpoidinvlem3  31113  grpoidinv  31115  nmobndseqi  31386  nmobndseqiALT  31387  hvaddsub4  31685  ocsh  31890  5oalem2  32262  5oalem5  32265  3oalem2  32270  pjjsi  32307  hoadddir  32411  leopmul  32741  stge1i  32845  hatomistici  32969  mdsymlem2  33011  mdsymlem5  33014  addltmulALT  33095  isoun  33342  fsumiunle  33466  lsmsnorb  33992  crefdf  34526  qqhre  34698  esumiun  34772  sxbrsigalem0  34949  dya2iocnei  34960  sxbrsigalem5  34966  sibfinima  35017  eulerpartlemgs2  35058  ballotlemfc0  35171  ballotlemfcc  35172  ballotlemsup  35183  bnj529  35418  bnj945  35450  bnj1098  35460  bnj1533  35528  bnj605  35583  bnj594  35588  bnj607  35592  bnj966  35620  bnj967  35621  bnj996  35632  bnj999  35634  bnj1006  35636  bnj1118  35660  bnj1172  35677  bnj1279  35694  bnj1296  35697  bnj1498  35737  fnrelpredd  35772  ptpconn  36084  cvmsi  36116  satf0op  36228  satffunlem1lem1  36253  satffunlem2lem1  36255  fv2ndcnv  36634  trisegint  36885  funtransport  36888  btwnconn1lem4  36947  btwnconn2  36959  segcon2  36962  outsideofeu  36988  isfne  37219  lukshef-ax2  37295  limsucncmpi  37325  weiunso  37346  bj-nsnid  38077  bj-restn0b  38104  bj-eldiag2  38191  bj-isrvec2  38314  pibt2  38433  unccur  38619  lindsadd  38629  poimirlem26  38657  poimirlem27  38658  poimirlem29  38660  poimirlem30  38661  poimirlem32  38663  heicant  38666  ismblfin  38672  itg2gt0cn  38686  areacirc  38724  impprop  38737  opelopab3  38745  isdivrngo  38977  isdrngo2  38985  fldcrngo  39031  flddmn  39085  refrelredund4  39744  mainer2  39985  cmtbr4N  40405  linepsubN  40902  pmapsub  40918  paddasslem14  40983  pclcmpatN  41051  trlval2  41313  cdleme20  41474  cdleme21j  41486  dvalveclem  42175  dia2dimlem7  42220  dvhlveclem  42258  docaclN  42274  dihjat1  42579  mapdhcl  42877  mapdh6dN  42889  mapdh8  42938  hdmap1l6d  42963  hdmap10  42990  hdmaprnlem17N  43013  hdmaplkr  43063  hdmapip0  43065  hgmapvv  43076  aks6d1c4  43267  cmpfiiin  43801  pellexlem4  43932  pellqrex  43979  acongtr  44078  acongrep  44080  jm2.23  44096  omlimcl2  44337  onsucf1lem  44364  oege1  44401  nnoeomeqom  44407  cantnfresb  44419  onmcl  44426  tfsconcat0i  44440  ofoafg  44449  ofoafo  44451  ofoaass  44455  ofoacom  44456  naddcnfass  44464  rp-fakeanorass  44607  rp-isfinite6  44612  harval3  44632  inintabss  44672  rfovcnvf1od  45097  clsk1indlem3  45136  ntrclsk13  45164  pm10.55  45446  refsum2cnlem1  46147  axccd2  46335  mptssid  46346  fmuldfeq  46688  climsuse  46713  limclner  46754  climxlim2lem  46948  icccncfext  46990  stoweidlem26  47129  stoweidlem52  47155  stoweidlem57  47160  fourierdlem20  47230  fourierdlem41  47251  fourierdlem52  47261  fourierdlem64  47273  fourierdlem102  47311  fourierdlem114  47323  ovolval4lem1  47752  preimagelt  47802  preimalegt  47803  squeezedltsq  48005  funressneu  48210  afvelrn  48331  elfz2z  48478  2ffzoeq  48491  zplusmodne  48512  addmodne  48513  minusmod5ne  48518  modn0mul  48526  m1modmmod  48527  nndivides2  48547  imasetpreimafvbijlemfv  48577  imasetpreimafvbijlemf1  48579  fargshiftfva  48618  ichreuopeq  48648  2exopprim  48700  reuopreuprim  48701  fmtnoprmfac1  48743  proththd  48792  opoeALTV  48874  evensumeven  48898  sbgoldbalt  48972  evengpop3  48989  evengpoap3  48990  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  wtgoldbnnsum4prm  48993  bgoldbnnsum3prm  48995  tgoldbach  49008  dfclnbgr6  49047  dfsclnbgr6  49049  uhgrimedg  49082  uhgrimprop  49083  isuspgrimlem  49086  isuspgrim  49087  gricushgr  49108  uhgrimisgrgric  49122  isubgr3stgrlem7  49163  uspgrlimlem2  49180  gpgedgel  49241  gpgprismgriedgdmss  49243  gpgedgvtx0  49252  gpgedgiov  49256  gpgedg2ov  49257  gpgedg2iv  49258  gpg5nbgrvtx03starlem2  49260  gpg5nbgrvtx13starlem1  49262  gpg5nbgrvtx13starlem3  49264  gpg5nbgrvtx03star  49271  gpg5nbgr3star  49272  gpg5gricstgr3  49281  pgnbgreunbgrlem4  49310  assintop  49399  uzlidlring  49425  2zrngnmrid  49446  cznrng  49451  lmodvsmdi  49584  lincsum  49634  lincsumcl  49636  el0ldep  49671  ldepspr  49678  lindssnlvec  49691  nn0digval  49805  1arympt1fv  49844  eenglngeehlnmlem1  49943  rrx2linest  49947  line2  49957  itsclc0yqe  49966  r19.41dv  50005  aacllem  51107