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  2570  r19.28v  3163  rmob  3841  eqeuel  4315  preq12nebg  4815  fores  6745  fdmeu  6878  ssimaex  6907  dffv2  6917  exfo  7038  fpropnf1  7201  f1ocoima  7237  oprabv  7406  ndmovass  7534  fun11uni  7863  resf1ext2b  7865  fabexgOLD  7869  f1oabexgOLD  7873  f1iun  7876  soxp  8059  tz7.48lem  8360  tz7.49c  8365  omass  8495  oewordri  8507  omabs  8566  sbthlem9  9008  pssnn  9078  fineqvlem  9150  domunfican  9206  fiint  9211  fsuppsssupp  9265  sup0  9351  inf1  9512  infeq5  9527  cantnfle  9561  rankuni  9753  djuunxp  9811  acndom  9939  acnnum  9940  cdainflem  10076  cfcof  10162  ac6num  10367  ac6s2  10374  brdom5  10417  brdom4  10418  genpnnp  10893  divmulasscom  11797  lediv2a  12013  supmul1  12088  infregelb  12103  nn2ge  12149  btwnz  12573  eluz2b2  12816  uz2mulcl  12821  eqreznegel  12829  xrsupexmnf  13201  xrinfmexpnf  13202  xrsupsslem  13203  xrinfmsslem  13204  supxrun  13212  ioo0  13267  elioo4g  13303  fz0fzelfz0  13531  fz0fzdiffz0  13534  2ffzeq  13546  elfzodifsumelfzo  13628  elfzom1elp1fzo  13629  zpnn0elfzo  13635  elfzom1elp1fzo1  13664  fzonfzoufzol  13668  quoremnn0  13757  zmodidfzoimp  13802  modabs  13805  modaddb  13810  modifeq2int  13837  modaddmulmod  13842  expcl2lem  13977  hashgt23el  14328  hashreshashfun  14343  iswrdsymb  14435  ccatcl  14478  ccatsymb  14487  swrdfv2  14566  swrdsbslen  14569  swrdspsleq  14570  pfxswrd  14610  pfxccatin12lem3  14636  pfxccatpfx2  14641  swrdccat3blem  14643  reuccatpfxs1  14651  repswccat  14690  cshweqdifid  14724  lswco  14743  repsco  14744  s4f1o  14822  trclun  14918  mulre  15025  rediv  15035  imdiv  15042  resqrex  15154  caurcvg2  15582  fsumdifsnconst  15695  modfsummods  15697  tanval  16034  p1modz1  16167  negdvdsb  16180  muldvds1  16188  muldvds2  16189  dvdscmulr  16192  dvdsmulcr  16193  sumodd  16296  divalglem8  16308  divgcdnn  16423  lcmfunsnlem2lem2  16547  lcmfun  16553  2mulprm  16601  maxprmfct  16617  vfermltlALT  16711  modprm0  16714  pcpremul  16752  pcmul  16760  oddprmdvds  16812  prmdvdsprmo  16951  cshwsidrepsw  17002  gsumccat  18746  grpissubg  19056  ecqusaddd  19102  ecqusaddcl  19103  eqg0subg  19106  gim0to0  19179  gsmsymgreqlem2  19341  symgfixfo  19349  fsfnn0gsumfsffz  19893  rnglz  20081  isringrng  20203  irredn0  20339  c0snmgmhm  20378  rimisrngim  20411  zrrnghm  20449  rnghmsubcsetclem2  20545  rhmsubcsetclem2  20574  rhmsubcrngclem2  20580  lsppratlem1  21082  qusmulrng  21217  quscrng  21218  rngqiprngghmlem3  21224  rngqiprnglinlem3  21228  rngqiprngimf1lem  21229  rngqiprnglin  21237  cnfldfunALT  21304  cnfldfunALTOLD  21317  dvdsrzring  21396  mpofrlmd  21712  matinvgcell  22348  mat1dimcrng  22390  dmatscmcl  22416  scmatscm  22426  scmatghm  22446  scmatmhm  22447  ma1repvcl  22483  slesolinv  22593  slesolinvbi  22594  cramerimplem1  22596  cramerimp  22599  cramerlem1  22600  cramer  22604  cpmatacl  22629  cpmatmcl  22632  mat2pmatghm  22643  mat2pmatmul  22644  m2pmfzgsumcl  22661  decpmatmul  22685  decpmatmulsumfsupp  22686  pmatcollpwfi  22695  pm2mpf1  22712  pm2mpghm  22729  pm2mpmhmlem1  22731  monmat2matmon  22737  chpdmatlem2  22752  chpdmat  22754  cpmadugsumlemB  22787  cpmadugsumlemC  22788  cpmadugsumlemF  22789  clscld  22960  neiptopnei  23045  2ndcdisj2  23370  comppfsc  23445  tx1stc  23563  opnfbas  23755  fbasfip  23781  alexsublem  23957  alexsubALTlem4  23963  cnextcn  23980  ngpocelbl  24617  cphipval  25168  bcthlem5  25253  vitalilem4  25537  vitalilem5  25538  itg2mulc  25673  bddiblnc  25768  dvcobr  25874  dvcobrOLD  25875  dvcnvlem  25905  dvferm1  25914  dvne0  25941  mdegmullem  26008  plyeq0lem  26140  plyexmo  26246  aalioulem5  26269  aalioulem6  26270  aaliou  26271  cxple2a  26633  cxpaddlelem  26686  cxpaddle  26687  relogbcxpb  26722  bcmono  27213  lgsprme0  27275  gausslemma2dlem0e  27296  gausslemma2dlem1a  27301  gausslemma2dlem6  27308  lgsquadlem2  27317  2lgsoddprm  27352  elno2  27591  cofcutr  27866  colinearalg  28886  axcontlem3  28942  umgrislfupgrlem  29098  edgupgr  29110  usgruspgrb  29159  usgrislfuspgr  29163  edgssv2  29174  umgr2edg  29185  uspgredg2v  29200  usgrexmplef  29235  subupgr  29263  subusgr  29265  nbupgrres  29340  nb3gr2nb  29360  nbupgruvtxres  29383  cusgrres  29425  cusgrsizeindslem  29428  cusgrsizeinds  29429  vtxdun  29458  finrusgrfusgr  29542  cusgrrusgr  29558  pthdifv  29706  spthdep  29710  cycliscrct  29775  crctcshwlkn0lem6  29791  crctcshwlkn0lem7  29792  crctcshtrl  29799  crctcsh  29800  umgr2adedgwlkonALT  29923  elwwlks2  29942  elwspths2spth  29943  rusgrnumwwlk  29951  clwlkclwwlklem2a  29973  clwlkclwwlklem3  29976  clwwisshclwws  29990  wwlksubclwwlk  30033  eleclclwwlknlem2  30036  eupth2lem3lem3  30205  eucrct2eupth1  30219  frgr3v  30250  3vfriswmgr  30253  1to3vfriswmgr  30255  3cyclfrgr  30263  vdgn1frgrv2  30271  frgrwopreglem5  30296  frgrwopreglem5ALT  30297  frrusgrord0lem  30314  frrusgrord0  30315  2clwwlk2clwwlk  30325  extwwlkfab  30327  numclwwlk1lem2fo  30333  friendshipgt3  30373  ex-natded9.20-2  30393  grpoidinvlem3  30481  grpoidinv  30483  nmobndseqi  30754  nmobndseqiALT  30755  hvaddsub4  31053  ocsh  31258  5oalem2  31630  5oalem5  31633  3oalem2  31638  pjjsi  31675  hoadddir  31779  leopmul  32109  stge1i  32213  hatomistici  32337  mdsymlem2  32379  mdsymlem5  32382  addltmulALT  32421  isoun  32678  fsumiunle  32807  lsmsnorb  33351  crefdf  33856  qqhre  34028  esumiun  34102  sxbrsigalem0  34279  dya2iocnei  34290  sxbrsigalem5  34296  sibfinima  34347  eulerpartlemgs2  34388  ballotlemfc0  34501  ballotlemfcc  34502  ballotlemsup  34513  bnj529  34748  bnj945  34780  bnj1098  34790  bnj1533  34859  bnj605  34914  bnj594  34919  bnj607  34923  bnj966  34951  bnj967  34952  bnj996  34963  bnj999  34965  bnj1006  34967  bnj1118  34991  bnj1172  35008  bnj1279  35025  bnj1296  35028  bnj1498  35068  fnrelpredd  35097  lfuhgr3  35152  loop1cycl  35169  cvmsi  35297  satf0op  35409  satffunlem1lem1  35434  satffunlem2lem1  35436  fv2ndcnv  35810  trisegint  36061  funtransport  36064  btwnconn1lem4  36123  btwnconn2  36135  segcon2  36138  outsideofeu  36164  isfne  36372  lukshef-ax2  36448  limsucncmpi  36478  weiunso  36499  bj-nsnid  37103  bj-restn0b  37124  bj-eldiag2  37210  bj-isrvec2  37333  pibt2  37450  unccur  37642  lindsadd  37652  lindsenlbs  37654  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem26  37685  poimirlem27  37686  poimirlem29  37688  poimirlem30  37689  poimirlem32  37691  heicant  37694  ismblfin  37700  itg2gt0cn  37714  areacirc  37752  opelopab3  37757  isdivrngo  37989  isdrngo2  37997  fldcrngo  38043  flddmn  38097  refrelredund4  38671  mainer2  38883  cmtbr4N  39293  linepsubN  39790  pmapsub  39806  paddasslem14  39871  pclcmpatN  39939  trlval2  40201  cdleme20  40362  cdleme21j  40374  dvalveclem  41063  dia2dimlem7  41108  dvhlveclem  41146  docaclN  41162  dihjat1  41467  mapdhcl  41765  mapdh6dN  41777  mapdh8  41826  hdmap1l6d  41851  hdmap10  41878  hdmaprnlem17N  41901  hdmaplkr  41951  hdmapip0  41953  hgmapvv  41964  aks6d1c4  42156  cmpfiiin  42729  pellexlem4  42864  pellqrex  42911  acongtr  43010  acongrep  43012  jm2.23  43028  omlimcl2  43274  onsucf1lem  43301  oege1  43338  nnoeomeqom  43344  cantnfresb  43356  onmcl  43363  tfsconcat0i  43377  ofoafg  43386  ofoafo  43388  ofoaass  43392  ofoacom  43393  naddcnfass  43401  rp-fakeanorass  43545  rp-isfinite6  43550  harval3  43570  inintabss  43610  rfovcnvf1od  44036  clsk1indlem3  44075  ntrclsk13  44103  pm10.55  44401  refsum2cnlem1  45073  axccd2  45266  mptssid  45277  fmuldfeq  45622  climsuse  45647  limclner  45688  climxlim2lem  45882  icccncfext  45924  stoweidlem26  46063  stoweidlem52  46089  stoweidlem57  46094  fourierdlem20  46164  fourierdlem41  46185  fourierdlem52  46195  fourierdlem64  46207  fourierdlem102  46245  fourierdlem114  46257  ovolval4lem1  46686  preimagelt  46736  preimalegt  46737  squeezedltsq  46916  funressneu  47077  afvelrn  47198  elfz2z  47345  2ffzoeq  47357  zplusmodne  47373  addmodne  47374  minusmod5ne  47379  modn0mul  47387  m1modmmod  47388  imasetpreimafvbijlemfv  47432  imasetpreimafvbijlemf1  47434  fargshiftfva  47473  ichreuopeq  47503  2exopprim  47555  reuopreuprim  47556  fmtnoprmfac1  47595  proththd  47644  opoeALTV  47713  evensumeven  47737  sbgoldbalt  47811  evengpop3  47828  evengpoap3  47829  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  wtgoldbnnsum4prm  47832  bgoldbnnsum3prm  47834  tgoldbach  47847  dfclnbgr6  47886  dfsclnbgr6  47888  uhgrimedg  47921  uhgrimprop  47922  isuspgrimlem  47925  isuspgrim  47926  gricushgr  47947  uhgrimisgrgric  47961  isubgr3stgrlem7  48002  uspgrlimlem2  48019  gpgedgel  48080  gpgprismgriedgdmss  48082  gpgedgvtx0  48091  gpgedgiov  48095  gpgedg2ov  48096  gpgedg2iv  48097  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem3  48103  gpg5nbgrvtx03star  48110  gpg5nbgr3star  48111  gpg5gricstgr3  48120  pgnbgreunbgrlem4  48149  assintop  48239  uzlidlring  48265  2zrngnmrid  48286  cznrng  48291  lmodvsmdi  48409  lincsum  48460  lincsumcl  48462  el0ldep  48497  ldepspr  48504  lindssnlvec  48517  nn0digval  48631  1arympt1fv  48670  eenglngeehlnmlem1  48768  rrx2linest  48773  line2  48783  itsclc0yqe  48792  r19.41dv  48832  setrec1lem3  49720  aacllem  49832