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  eu6im  2602  r19.28v  3195  rmob  3840  eqeuel  4316  preq12nebg  4826  fores  6803  fdmeu  6938  ssimaex  6967  dffv2  6977  exfo  7102  fpropnf1  7268  f1ocoima  7308  oprabv  7477  ndmovass  7606  fun11uni  7934  resf1ext2b  7936  f1iun  7945  soxp  8131  tz7.48lem  8434  tz7.49c  8439  omass  8571  oewordri  8584  omabs  8643  sbthlem9  9097  pssnn  9167  fineqvlem  9240  domunfican  9295  fiint  9300  fsuppsssupp  9355  sup0  9441  inf1  9605  infeq5  9620  cantnfle  9654  rankuni  9849  djuunxp  9930  acndom  10058  acnnum  10059  cdainflem  10194  cfcof  10280  ac6num  10485  ac6s2  10492  brdom5  10536  brdom4  10537  genpnnp  11018  divmulasscom  11924  lediv2a  12137  supmul1  12212  infregelb  12227  nn2ge  12291  btwnz  12728  eluz2b2  12974  uz2mulcl  12979  eqreznegel  12987  xrsupexmnf  13361  xrinfmexpnf  13362  xrsupsslem  13363  xrinfmsslem  13364  supxrun  13372  ioo0  13427  elioo4g  13463  fz0fzelfz0  13693  fz0fzdiffz0  13696  2ffzeq  13708  elfzodifsumelfzo  13791  elfzom1elp1fzo  13792  zpnn0elfzo  13798  elfzom1elp1fzo1  13827  fzonfzoufzol  13831  quoremnn0  13921  zmodidfzoimp  13966  modabs  13969  modaddb  13974  modifeq2int  14001  modaddmulmod  14006  expcl2lem  14141  hashgt23el  14493  hashreshashfun  14508  iswrdsymb  14600  ccatcl  14643  ccatsymb  14652  swrdfv2  14735  swrdsbslen  14738  swrdspsleq  14739  pfxswrd  14779  pfxccatin12lem3  14805  pfxccatpfx2  14810  swrdccat3blem  14812  reuccatpfxs1  14820  repswccat  14861  cshweqdifid  14895  lswco  14914  repsco  14915  s4f1o  14993  trclun  15091  mulre  15212  rediv  15222  imdiv  15229  resqrex  15341  caurcvg2  15769  fsumdifsnconst  15882  modfsummods  15884  tanval  16222  p1modz1  16355  negdvdsb  16368  muldvds1  16376  muldvds2  16377  dvdscmulr  16380  dvdsmulcr  16381  sumodd  16484  divalglem8  16496  divgcdnn  16611  lcmfunsnlem2lem2  16735  lcmfun  16741  2mulprm  16789  maxprmfct  16806  vfermltlALT  16900  modprm0  16903  pcpremul  16941  pcmul  16949  oddprmdvds  17001  prmdvdsprmo  17140  cshwsidrepsw  17191  gsumccat  18956  grpissubg  19276  ecqusaddd  19326  ecqusaddcl  19327  eqg0subg  19330  gim0to0  19402  gsmsymgreqlem2  19564  symgfixfo  19572  fsfnn0gsumfsffz  20116  rnglz  20306  isringrng  20434  irredn0  20570  c0snmgmhm  20609  rimisrngim  20652  zrrnghm  20704  rnghmsubcsetclem2  20800  rhmsubcsetclem2  20829  rhmsubcrngclem2  20835  lsppratlem1  21340  qusmulrng  21491  quscrng  21492  rngqiprngghmlem3  21498  rngqiprnglinlem3  21502  rngqiprngimf1lem  21503  rngqiprnglin  21511  cnfldfunALT  21606  dvdsrzring  21680  mpofrlmd  21996  lindsenlbs  22070  matinvgcell  22663  mat1dimcrng  22705  dmatscmcl  22731  scmatscm  22741  scmatghm  22761  scmatmhm  22762  ma1repvcl  22798  matunitlindflem1  22907  matunitlindflem2  22908  slesolinv  22911  slesolinvbi  22912  cramerimplem1  22914  cramerimp  22917  cramerlem1  22918  cramer  22922  cpmatacl  22947  cpmatmcl  22950  mat2pmatghm  22961  mat2pmatmul  22962  m2pmfzgsumcl  22979  decpmatmul  23003  decpmatmulsumfsupp  23004  pmatcollpwfi  23013  pm2mpf1  23030  pm2mpghm  23047  pm2mpmhmlem1  23049  monmat2matmon  23055  chpdmatlem2  23070  chpdmat  23072  cpmadugsumlemB  23105  cpmadugsumlemC  23106  cpmadugsumlemF  23107  clscld  23278  neiptopnei  23363  2ndcdisj2  23689  comppfsc  23764  tx1stc  23882  opnfbas  24074  fbasfip  24100  alexsublem  24276  alexsubALTlem4  24282  cnextcn  24299  ngpocelbl  24936  cphipval  25477  bcthlem5  25562  vitalilem4  25845  vitalilem5  25846  itg2mulc  25981  bddiblnc  26076  dvcobr  26180  dvcnvlem  26210  dvferm1  26219  dvne0  26245  mdegmullem  26310  plyeq0lem  26443  plyexmo  26552  aalioulem5  26579  aalioulem6  26580  aaliou  26581  cxple2a  26944  cxpaddlelem  26996  cxpaddle  26997  relogbcxpb  27032  bcmono  27521  lgsprme0  27583  gausslemma2dlem0e  27604  gausslemma2dlem1a  27609  gausslemma2dlem6  27616  lgsquadlem2  27625  2lgsoddprm  27660  elno2  27898  cofcutr  28197  colinearalg  29375  axcontlem3  29431  umgrislfupgrlem  29587  edgupgr  29599  lfuhgr3  29615  usgruspgrb  29651  usgrislfuspgr  29655  edgssv2  29666  umgr2edg  29677  uspgredg2v  29692  usgrexmplef  29727  subupgr  29755  subusgr  29757  nbupgrres  29832  nb3gr2nb  29852  nbupgruvtxres  29875  cusgrres  29916  cusgrsizeindslem  29919  cusgrsizeinds  29920  vtxdun  29949  finrusgrfusgr  30033  cusgrrusgr  30049  pthdifv  30203  spthdep  30207  cycliscrct  30274  crctcshwlkn0lem6  30291  crctcshwlkn0lem7  30292  crctcshtrl  30299  crctcsh  30300  umgr2adedgwlkonALT  30423  elwwlks2  30445  elwspths2spth  30446  rusgrnumwwlk  30454  clwlkclwwlklem2a  30476  clwlkclwwlklem3  30479  clwwisshclwws  30493  wwlksubclwwlk  30536  eleclclwwlknlem2  30539  loop1cycl  30631  eupth2lem3lem3  30718  eucrct2eupth1  30732  frgr3v  30763  3vfriswmgr  30766  1to3vfriswmgr  30768  3cyclfrgr  30776  vdgn1frgrv2  30784  frgrwopreglem5  30809  frgrwopreglem5ALT  30810  frrusgrord0lem  30827  frrusgrord0  30828  2clwwlk2clwwlk  30838  extwwlkfab  30840  numclwwlk1lem2fo  30846  friendshipgt3  30886  ex-natded9.20-2  30906  grpoidinvlem3  30995  grpoidinv  30997  nmobndseqi  31268  nmobndseqiALT  31269  hvaddsub4  31567  ocsh  31772  5oalem2  32144  5oalem5  32147  3oalem2  32152  pjjsi  32189  hoadddir  32293  leopmul  32623  stge1i  32727  hatomistici  32851  mdsymlem2  32893  mdsymlem5  32896  addltmulALT  32935  isoun  33182  fsumiunle  33307  lsmsnorb  33832  crefdf  34366  qqhre  34538  esumiun  34612  sxbrsigalem0  34790  dya2iocnei  34801  sxbrsigalem5  34807  sibfinima  34858  eulerpartlemgs2  34899  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemsup  35024  bnj529  35259  bnj945  35291  bnj1098  35301  bnj1533  35369  bnj605  35424  bnj594  35429  bnj607  35433  bnj966  35461  bnj967  35462  bnj996  35473  bnj999  35475  bnj1006  35477  bnj1118  35501  bnj1172  35518  bnj1279  35535  bnj1296  35538  bnj1498  35578  fnrelpredd  35604  cvmsi  35852  satf0op  35964  satffunlem1lem1  35989  satffunlem2lem1  35991  fv2ndcnv  36365  trisegint  36616  funtransport  36619  btwnconn1lem4  36678  btwnconn2  36690  segcon2  36693  outsideofeu  36719  isfne  36966  lukshef-ax2  37042  limsucncmpi  37072  weiunso  37093  bj-nsnid  37822  bj-restn0b  37849  bj-eldiag2  37937  bj-isrvec2  38060  pibt2  38179  unccur  38365  lindsadd  38375  poimirlem26  38403  poimirlem27  38404  poimirlem29  38406  poimirlem30  38407  poimirlem32  38409  heicant  38412  ismblfin  38418  itg2gt0cn  38432  areacirc  38470  opelopab3  38476  isdivrngo  38708  isdrngo2  38716  fldcrngo  38762  flddmn  38816  refrelredund4  39475  mainer2  39716  cmtbr4N  40136  linepsubN  40633  pmapsub  40649  paddasslem14  40714  pclcmpatN  40782  trlval2  41044  cdleme20  41205  cdleme21j  41217  dvalveclem  41906  dia2dimlem7  41951  dvhlveclem  41989  docaclN  42005  dihjat1  42310  mapdhcl  42608  mapdh6dN  42620  mapdh8  42669  hdmap1l6d  42694  hdmap10  42721  hdmaprnlem17N  42744  hdmaplkr  42794  hdmapip0  42796  hgmapvv  42807  aks6d1c4  42998  cmpfiiin  43550  pellexlem4  43681  pellqrex  43728  acongtr  43827  acongrep  43829  jm2.23  43845  omlimcl2  44091  onsucf1lem  44118  oege1  44155  nnoeomeqom  44161  cantnfresb  44173  onmcl  44180  tfsconcat0i  44194  ofoafg  44203  ofoafo  44205  ofoaass  44209  ofoacom  44210  naddcnfass  44218  rp-fakeanorass  44361  rp-isfinite6  44366  harval3  44386  inintabss  44426  rfovcnvf1od  44852  clsk1indlem3  44891  ntrclsk13  44919  pm10.55  45201  refsum2cnlem1  45879  axccd2  46067  mptssid  46078  fmuldfeq  46421  climsuse  46446  limclner  46487  climxlim2lem  46681  icccncfext  46723  stoweidlem26  46862  stoweidlem52  46888  stoweidlem57  46893  fourierdlem20  46963  fourierdlem41  46984  fourierdlem52  46994  fourierdlem64  47006  fourierdlem102  47044  fourierdlem114  47056  ovolval4lem1  47485  preimagelt  47535  preimalegt  47536  squeezedltsq  47738  funressneu  47943  afvelrn  48064  elfz2z  48211  2ffzoeq  48224  zplusmodne  48245  addmodne  48246  minusmod5ne  48251  modn0mul  48259  m1modmmod  48260  nndivides2  48280  imasetpreimafvbijlemfv  48310  imasetpreimafvbijlemf1  48312  fargshiftfva  48351  ichreuopeq  48381  2exopprim  48433  reuopreuprim  48434  fmtnoprmfac1  48476  proththd  48525  opoeALTV  48607  evensumeven  48631  sbgoldbalt  48705  evengpop3  48722  evengpoap3  48723  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  wtgoldbnnsum4prm  48726  bgoldbnnsum3prm  48728  tgoldbach  48741  dfclnbgr6  48780  dfsclnbgr6  48782  uhgrimedg  48815  uhgrimprop  48816  isuspgrimlem  48819  isuspgrim  48820  gricushgr  48841  uhgrimisgrgric  48855  isubgr3stgrlem7  48896  uspgrlimlem2  48913  gpgedgel  48974  gpgprismgriedgdmss  48976  gpgedgvtx0  48985  gpgedgiov  48989  gpgedg2ov  48990  gpgedg2iv  48991  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem3  48997  gpg5nbgrvtx03star  49004  gpg5nbgr3star  49005  gpg5gricstgr3  49014  pgnbgreunbgrlem4  49043  assintop  49132  uzlidlring  49158  2zrngnmrid  49179  cznrng  49184  lmodvsmdi  49317  lincsum  49367  lincsumcl  49369  el0ldep  49404  ldepspr  49411  lindssnlvec  49424  nn0digval  49538  1arympt1fv  49577  eenglngeehlnmlem1  49675  rrx2linest  49680  line2  49690  itsclc0yqe  49699  r19.41dv  49738  setrec1lem3  50623  aacllem  50780