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  2572  r19.28v  3164  rmob  3837  eqeuel  4314  preq12nebg  4814  fores  6750  fdmeu  6884  ssimaex  6913  dffv2  6923  exfo  7044  fpropnf1  7207  f1ocoima  7243  oprabv  7412  ndmovass  7540  fun11uni  7869  resf1ext2b  7871  fabexgOLD  7875  f1oabexgOLD  7879  f1iun  7882  soxp  8065  tz7.48lem  8366  tz7.49c  8371  omass  8501  oewordri  8513  omabs  8572  sbthlem9  9015  pssnn  9085  fineqvlem  9157  domunfican  9213  fiint  9218  fsuppsssupp  9272  sup0  9358  inf1  9519  infeq5  9534  cantnfle  9568  rankuni  9763  djuunxp  9821  acndom  9949  acnnum  9950  cdainflem  10086  cfcof  10172  ac6num  10377  ac6s2  10384  brdom5  10427  brdom4  10428  genpnnp  10903  divmulasscom  11807  lediv2a  12023  supmul1  12098  infregelb  12113  nn2ge  12159  btwnz  12582  eluz2b2  12821  uz2mulcl  12826  eqreznegel  12834  xrsupexmnf  13206  xrinfmexpnf  13207  xrsupsslem  13208  xrinfmsslem  13209  supxrun  13217  ioo0  13272  elioo4g  13308  fz0fzelfz0  13536  fz0fzdiffz0  13539  2ffzeq  13551  elfzodifsumelfzo  13633  elfzom1elp1fzo  13634  zpnn0elfzo  13640  elfzom1elp1fzo1  13669  fzonfzoufzol  13673  quoremnn0  13762  zmodidfzoimp  13807  modabs  13810  modaddb  13815  modifeq2int  13842  modaddmulmod  13847  expcl2lem  13982  hashgt23el  14333  hashreshashfun  14348  iswrdsymb  14440  ccatcl  14483  ccatsymb  14492  swrdfv2  14571  swrdsbslen  14574  swrdspsleq  14575  pfxswrd  14615  pfxccatin12lem3  14641  pfxccatpfx2  14646  swrdccat3blem  14648  reuccatpfxs1  14656  repswccat  14695  cshweqdifid  14729  lswco  14748  repsco  14749  s4f1o  14827  trclun  14923  mulre  15030  rediv  15040  imdiv  15047  resqrex  15159  caurcvg2  15587  fsumdifsnconst  15700  modfsummods  15702  tanval  16039  p1modz1  16172  negdvdsb  16185  muldvds1  16193  muldvds2  16194  dvdscmulr  16197  dvdsmulcr  16198  sumodd  16301  divalglem8  16313  divgcdnn  16428  lcmfunsnlem2lem2  16552  lcmfun  16558  2mulprm  16606  maxprmfct  16622  vfermltlALT  16716  modprm0  16719  pcpremul  16757  pcmul  16765  oddprmdvds  16817  prmdvdsprmo  16956  cshwsidrepsw  17007  gsumccat  18751  grpissubg  19061  ecqusaddd  19106  ecqusaddcl  19107  eqg0subg  19110  gim0to0  19183  gsmsymgreqlem2  19345  symgfixfo  19353  fsfnn0gsumfsffz  19897  rnglz  20085  isringrng  20207  irredn0  20343  c0snmgmhm  20382  rimisrngim  20415  zrrnghm  20453  rnghmsubcsetclem2  20549  rhmsubcsetclem2  20578  rhmsubcrngclem2  20584  lsppratlem1  21086  qusmulrng  21221  quscrng  21222  rngqiprngghmlem3  21228  rngqiprnglinlem3  21232  rngqiprngimf1lem  21233  rngqiprnglin  21241  cnfldfunALT  21308  cnfldfunALTOLD  21321  dvdsrzring  21400  mpofrlmd  21716  matinvgcell  22351  mat1dimcrng  22393  dmatscmcl  22419  scmatscm  22429  scmatghm  22449  scmatmhm  22450  ma1repvcl  22486  slesolinv  22596  slesolinvbi  22597  cramerimplem1  22599  cramerimp  22602  cramerlem1  22603  cramer  22607  cpmatacl  22632  cpmatmcl  22635  mat2pmatghm  22646  mat2pmatmul  22647  m2pmfzgsumcl  22664  decpmatmul  22688  decpmatmulsumfsupp  22689  pmatcollpwfi  22698  pm2mpf1  22715  pm2mpghm  22732  pm2mpmhmlem1  22734  monmat2matmon  22740  chpdmatlem2  22755  chpdmat  22757  cpmadugsumlemB  22790  cpmadugsumlemC  22791  cpmadugsumlemF  22792  clscld  22963  neiptopnei  23048  2ndcdisj2  23373  comppfsc  23448  tx1stc  23566  opnfbas  23758  fbasfip  23784  alexsublem  23960  alexsubALTlem4  23966  cnextcn  23983  ngpocelbl  24620  cphipval  25171  bcthlem5  25256  vitalilem4  25540  vitalilem5  25541  itg2mulc  25676  bddiblnc  25771  dvcobr  25877  dvcobrOLD  25878  dvcnvlem  25908  dvferm1  25917  dvne0  25944  mdegmullem  26011  plyeq0lem  26143  plyexmo  26249  aalioulem5  26272  aalioulem6  26273  aaliou  26274  cxple2a  26636  cxpaddlelem  26689  cxpaddle  26690  relogbcxpb  26725  bcmono  27216  lgsprme0  27278  gausslemma2dlem0e  27299  gausslemma2dlem1a  27304  gausslemma2dlem6  27311  lgsquadlem2  27320  2lgsoddprm  27355  elno2  27594  cofcutr  27869  colinearalg  28890  axcontlem3  28946  umgrislfupgrlem  29102  edgupgr  29114  usgruspgrb  29163  usgrislfuspgr  29167  edgssv2  29178  umgr2edg  29189  uspgredg2v  29204  usgrexmplef  29239  subupgr  29267  subusgr  29269  nbupgrres  29344  nb3gr2nb  29364  nbupgruvtxres  29387  cusgrres  29429  cusgrsizeindslem  29432  cusgrsizeinds  29433  vtxdun  29462  finrusgrfusgr  29546  cusgrrusgr  29562  pthdifv  29710  spthdep  29714  cycliscrct  29779  crctcshwlkn0lem6  29795  crctcshwlkn0lem7  29796  crctcshtrl  29803  crctcsh  29804  umgr2adedgwlkonALT  29927  elwwlks2  29949  elwspths2spth  29950  rusgrnumwwlk  29958  clwlkclwwlklem2a  29980  clwlkclwwlklem3  29983  clwwisshclwws  29997  wwlksubclwwlk  30040  eleclclwwlknlem2  30043  eupth2lem3lem3  30212  eucrct2eupth1  30226  frgr3v  30257  3vfriswmgr  30260  1to3vfriswmgr  30262  3cyclfrgr  30270  vdgn1frgrv2  30278  frgrwopreglem5  30303  frgrwopreglem5ALT  30304  frrusgrord0lem  30321  frrusgrord0  30322  2clwwlk2clwwlk  30332  extwwlkfab  30334  numclwwlk1lem2fo  30340  friendshipgt3  30380  ex-natded9.20-2  30400  grpoidinvlem3  30488  grpoidinv  30490  nmobndseqi  30761  nmobndseqiALT  30762  hvaddsub4  31060  ocsh  31265  5oalem2  31637  5oalem5  31640  3oalem2  31645  pjjsi  31682  hoadddir  31786  leopmul  32116  stge1i  32220  hatomistici  32344  mdsymlem2  32386  mdsymlem5  32389  addltmulALT  32428  isoun  32687  fsumiunle  32817  lsmsnorb  33363  crefdf  33882  qqhre  34054  esumiun  34128  sxbrsigalem0  34305  dya2iocnei  34316  sxbrsigalem5  34322  sibfinima  34373  eulerpartlemgs2  34414  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemsup  34539  bnj529  34774  bnj945  34806  bnj1098  34816  bnj1533  34885  bnj605  34940  bnj594  34945  bnj607  34949  bnj966  34977  bnj967  34978  bnj996  34989  bnj999  34991  bnj1006  34993  bnj1118  35017  bnj1172  35034  bnj1279  35051  bnj1296  35054  bnj1498  35094  fnrelpredd  35123  lfuhgr3  35185  loop1cycl  35202  cvmsi  35330  satf0op  35442  satffunlem1lem1  35467  satffunlem2lem1  35469  fv2ndcnv  35843  trisegint  36093  funtransport  36096  btwnconn1lem4  36155  btwnconn2  36167  segcon2  36170  outsideofeu  36196  isfne  36404  lukshef-ax2  36480  limsucncmpi  36510  weiunso  36531  bj-nsnid  37135  bj-restn0b  37156  bj-eldiag2  37242  bj-isrvec2  37365  pibt2  37482  unccur  37663  lindsadd  37673  lindsenlbs  37675  matunitlindflem1  37676  matunitlindflem2  37677  poimirlem26  37706  poimirlem27  37707  poimirlem29  37709  poimirlem30  37710  poimirlem32  37712  heicant  37715  ismblfin  37721  itg2gt0cn  37735  areacirc  37773  opelopab3  37778  isdivrngo  38010  isdrngo2  38018  fldcrngo  38064  flddmn  38118  refrelredund4  38751  mainer2  38964  cmtbr4N  39374  linepsubN  39871  pmapsub  39887  paddasslem14  39952  pclcmpatN  40020  trlval2  40282  cdleme20  40443  cdleme21j  40455  dvalveclem  41144  dia2dimlem7  41189  dvhlveclem  41227  docaclN  41243  dihjat1  41548  mapdhcl  41846  mapdh6dN  41858  mapdh8  41907  hdmap1l6d  41932  hdmap10  41959  hdmaprnlem17N  41982  hdmaplkr  42032  hdmapip0  42034  hgmapvv  42045  aks6d1c4  42237  cmpfiiin  42814  pellexlem4  42949  pellqrex  42996  acongtr  43095  acongrep  43097  jm2.23  43113  omlimcl2  43359  onsucf1lem  43386  oege1  43423  nnoeomeqom  43429  cantnfresb  43441  onmcl  43448  tfsconcat0i  43462  ofoafg  43471  ofoafo  43473  ofoaass  43477  ofoacom  43478  naddcnfass  43486  rp-fakeanorass  43630  rp-isfinite6  43635  harval3  43655  inintabss  43695  rfovcnvf1od  44121  clsk1indlem3  44160  ntrclsk13  44188  pm10.55  44486  refsum2cnlem1  45158  axccd2  45351  mptssid  45362  fmuldfeq  45707  climsuse  45732  limclner  45773  climxlim2lem  45967  icccncfext  46009  stoweidlem26  46148  stoweidlem52  46174  stoweidlem57  46179  fourierdlem20  46249  fourierdlem41  46270  fourierdlem52  46280  fourierdlem64  46292  fourierdlem102  46330  fourierdlem114  46342  ovolval4lem1  46771  preimagelt  46821  preimalegt  46822  squeezedltsq  47010  funressneu  47171  afvelrn  47292  elfz2z  47439  2ffzoeq  47451  zplusmodne  47467  addmodne  47468  minusmod5ne  47473  modn0mul  47481  m1modmmod  47482  imasetpreimafvbijlemfv  47526  imasetpreimafvbijlemf1  47528  fargshiftfva  47567  ichreuopeq  47597  2exopprim  47649  reuopreuprim  47650  fmtnoprmfac1  47689  proththd  47738  opoeALTV  47807  evensumeven  47831  sbgoldbalt  47905  evengpop3  47922  evengpoap3  47923  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  wtgoldbnnsum4prm  47926  bgoldbnnsum3prm  47928  tgoldbach  47941  dfclnbgr6  47980  dfsclnbgr6  47982  uhgrimedg  48015  uhgrimprop  48016  isuspgrimlem  48019  isuspgrim  48020  gricushgr  48041  uhgrimisgrgric  48055  isubgr3stgrlem7  48096  uspgrlimlem2  48113  gpgedgel  48174  gpgprismgriedgdmss  48176  gpgedgvtx0  48185  gpgedgiov  48189  gpgedg2ov  48190  gpgedg2iv  48191  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem3  48197  gpg5nbgrvtx03star  48204  gpg5nbgr3star  48205  gpg5gricstgr3  48214  pgnbgreunbgrlem4  48243  assintop  48333  uzlidlring  48359  2zrngnmrid  48380  cznrng  48385  lmodvsmdi  48503  lincsum  48554  lincsumcl  48556  el0ldep  48591  ldepspr  48598  lindssnlvec  48611  nn0digval  48725  1arympt1fv  48764  eenglngeehlnmlem1  48862  rrx2linest  48867  line2  48877  itsclc0yqe  48886  r19.41dv  48926  setrec1lem3  49814  aacllem  49926