Theorem anim1i 614

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 612	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 206  df-an 396

This theorem is referenced by:  sylanl1  679  sylanr1  681  eu6im  2565  r19.28v  3185  rmob  3881  eqeuel  4359  preq12nebg  4860  fores  6816  fdmeu  6950  ssimaex  6978  dffv2  6988  exfo  7110  fpropnf1  7272  oprabv  7475  ndmovass  7604  fun11uni  7935  fabexg  7937  f1oabexg  7939  f1iun  7942  soxp  8129  tz7.48lem  8456  tz7.49c  8461  omass  8595  oewordri  8607  omabs  8666  sbthlem9  9110  pssnn  9187  fineqvlem  9281  pssnnOLD  9284  domunfican  9339  fiint  9343  fsuppsssupp  9399  sup0  9484  inf1  9640  infeq5  9655  cantnfle  9689  rankuni  9881  djuunxp  9939  acndom  10069  acnnum  10070  cdainflem  10205  cfcof  10292  ac6num  10497  ac6s2  10504  brdom5  10547  brdom4  10548  genpnnp  11023  divmulasscom  11921  lediv2a  12133  supmul1  12208  infregelb  12223  nn2ge  12264  btwnz  12690  eluz2b2  12930  uz2mulcl  12935  eqreznegel  12943  xrsupexmnf  13311  xrinfmexpnf  13312  xrsupsslem  13313  xrinfmsslem  13314  supxrun  13322  ioo0  13376  elioo4g  13411  fz0fzelfz0  13634  fz0fzdiffz0  13637  2ffzeq  13649  elfzodifsumelfzo  13725  elfzom1elp1fzo  13726  zpnn0elfzo  13732  elfzom1elp1fzo1  13759  fzonfzoufzol  13762  quoremnn0  13848  zmodidfzoimp  13893  modabs  13896  modmuladd  13905  modifeq2int  13925  modaddmulmod  13930  expcl2lem  14065  hashgt23el  14410  hashreshashfun  14425  iswrdsymb  14508  ccatcl  14551  ccatsymb  14559  swrdfv2  14638  swrdsbslen  14641  swrdspsleq  14642  pfxswrd  14683  pfxccatin12lem3  14709  pfxccatpfx2  14714  swrdccat3blem  14716  reuccatpfxs1  14724  repswccat  14763  cshweqdifid  14797  lswco  14817  repsco  14818  s4f1o  14896  trclun  14988  mulre  15095  rediv  15105  imdiv  15112  resqrex  15224  caurcvg2  15651  fsumdifsnconst  15764  modfsummods  15766  tanval  16099  p1modz1  16232  negdvdsb  16244  muldvds1  16252  muldvds2  16253  dvdscmulr  16256  dvdsmulcr  16257  sumodd  16359  divalglem8  16371  divgcdnn  16484  lcmfunsnlem2lem2  16604  lcmfun  16610  2mulprm  16658  maxprmfct  16674  vfermltlALT  16765  modprm0  16768  pcpremul  16806  pcmul  16814  oddprmdvds  16866  prmdvdsprmo  17005  cshwsidrepsw  17057  gsumccat  18787  grpissubg  19095  ecqusaddd  19141  ecqusaddcl  19142  eqg0subg  19145  gim0to0  19217  gsmsymgreqlem2  19380  symgfixfo  19388  fsfnn0gsumfsffz  19932  rnglz  20099  isringrng  20217  irredn0  20356  c0snmgmhm  20395  rimisrngim  20431  zrrnghm  20467  rnghmsubcsetclem2  20559  rhmsubcsetclem2  20588  rhmsubcrngclem2  20594  lsppratlem1  21029  qusmulrng  21168  quscrng  21169  rngqiprngghmlem3  21173  rngqiprnglinlem3  21177  rngqiprngimf1lem  21178  rngqiprnglin  21186  cnfldfunALT  21288  cnfldfunALTOLD  21301  dvdsrzring  21381  mpofrlmd  21705  matinvgcell  22331  mat1dimcrng  22373  dmatscmcl  22399  scmatscm  22409  scmatghm  22429  scmatmhm  22430  ma1repvcl  22466  slesolinv  22576  slesolinvbi  22577  cramerimplem1  22579  cramerimp  22582  cramerlem1  22583  cramer  22587  cpmatacl  22612  cpmatmcl  22615  mat2pmatghm  22626  mat2pmatmul  22627  m2pmfzgsumcl  22644  decpmatmul  22668  decpmatmulsumfsupp  22669  pmatcollpwfi  22678  pm2mpf1  22695  pm2mpghm  22712  pm2mpmhmlem1  22714  monmat2matmon  22720  chpdmatlem2  22735  chpdmat  22737  cpmadugsumlemB  22770  cpmadugsumlemC  22771  cpmadugsumlemF  22772  clscld  22945  neiptopnei  23030  2ndcdisj2  23355  comppfsc  23430  tx1stc  23548  opnfbas  23740  fbasfip  23766  alexsublem  23942  alexsubALTlem4  23948  cnextcn  23965  ngpocelbl  24615  cphipval  25165  bcthlem5  25250  vitalilem4  25534  vitalilem5  25535  itg2mulc  25671  bddiblnc  25765  dvcobr  25871  dvcobrOLD  25872  dvcnvlem  25902  dvferm1  25911  dvne0  25938  mdegmullem  26008  plyeq0lem  26138  plyexmo  26242  aalioulem5  26265  aalioulem6  26266  aaliou  26267  cxple2a  26627  cxpaddlelem  26680  cxpaddle  26681  relogbcxpb  26713  bcmono  27204  lgsprme0  27266  gausslemma2dlem0e  27287  gausslemma2dlem1a  27292  gausslemma2dlem6  27299  lgsquadlem2  27308  2lgsoddprm  27343  elno2  27581  cofcutr  27838  colinearalg  28715  axcontlem3  28771  umgrislfupgrlem  28929  edgupgr  28941  usgruspgrb  28990  usgrislfuspgr  28994  edgssv2  29005  umgr2edg  29016  uspgredg2v  29031  usgrexmplef  29066  subupgr  29094  subusgr  29096  nbupgrres  29171  nb3gr2nb  29191  nbupgruvtxres  29214  cusgrres  29256  cusgrsizeindslem  29259  cusgrsizeinds  29260  vtxdun  29289  finrusgrfusgr  29373  cusgrrusgr  29389  spthdep  29542  cycliscrct  29607  crctcshwlkn0lem6  29620  crctcshwlkn0lem7  29621  crctcshtrl  29628  crctcsh  29629  umgr2adedgwlkonALT  29752  elwwlks2  29771  elwspths2spth  29772  rusgrnumwwlk  29780  clwlkclwwlklem2a  29802  clwlkclwwlklem3  29805  clwwisshclwws  29819  wwlksubclwwlk  29862  eleclclwwlknlem2  29865  eupth2lem3lem3  30034  eucrct2eupth1  30048  frgr3v  30079  3vfriswmgr  30082  1to3vfriswmgr  30084  3cyclfrgr  30092  vdgn1frgrv2  30100  frgrwopreglem5  30125  frgrwopreglem5ALT  30126  frrusgrord0lem  30143  frrusgrord0  30144  2clwwlk2clwwlk  30154  extwwlkfab  30156  numclwwlk1lem2fo  30162  friendshipgt3  30202  ex-natded9.20-2  30222  grpoidinvlem3  30310  grpoidinv  30312  nmobndseqi  30583  nmobndseqiALT  30584  hvaddsub4  30882  ocsh  31087  5oalem2  31459  5oalem5  31462  3oalem2  31467  pjjsi  31504  hoadddir  31608  leopmul  31938  stge1i  32042  hatomistici  32166  mdsymlem2  32208  mdsymlem5  32211  addltmulALT  32250  isoun  32476  fsumiunle  32587  lsmsnorb  33095  crefdf  33444  qqhre  33616  esumiun  33708  sxbrsigalem0  33886  dya2iocnei  33897  sxbrsigalem5  33903  sibfinima  33954  eulerpartlemgs2  33995  ballotlemfc0  34107  ballotlemfcc  34108  ballotlemsup  34119  bnj529  34367  bnj945  34399  bnj1098  34409  bnj1533  34478  bnj605  34533  bnj594  34538  bnj607  34542  bnj966  34570  bnj967  34571  bnj996  34582  bnj999  34584  bnj1006  34586  bnj1118  34610  bnj1172  34627  bnj1279  34644  bnj1296  34647  bnj1498  34687  fnrelpredd  34707  lfuhgr3  34724  loop1cycl  34742  cvmsi  34870  satf0op  34982  satffunlem1lem1  35007  satffunlem2lem1  35009  fv2ndcnv  35368  trisegint  35619  funtransport  35622  btwnconn1lem4  35681  btwnconn2  35693  segcon2  35696  outsideofeu  35722  isfne  35818  lukshef-ax2  35894  limsucncmpi  35924  bj-nsnid  36544  bj-restn0b  36565  bj-eldiag2  36651  bj-isrvec2  36774  pibt2  36891  unccur  37071  lindsadd  37081  lindsenlbs  37083  matunitlindflem1  37084  matunitlindflem2  37085  poimirlem26  37114  poimirlem27  37115  poimirlem29  37117  poimirlem30  37118  poimirlem32  37120  heicant  37123  ismblfin  37129  itg2gt0cn  37143  areacirc  37181  opelopab3  37186  isdivrngo  37418  isdrngo2  37426  fldcrngo  37472  flddmn  37526  refrelredund4  38102  mainer2  38313  cmtbr4N  38722  linepsubN  39220  pmapsub  39236  paddasslem14  39301  pclcmpatN  39369  trlval2  39631  cdleme20  39792  cdleme21j  39804  dvalveclem  40493  dia2dimlem7  40538  dvhlveclem  40576  docaclN  40592  dihjat1  40897  mapdhcl  41195  mapdh6dN  41207  mapdh8  41256  hdmap1l6d  41281  hdmap10  41308  hdmaprnlem17N  41331  hdmaplkr  41381  hdmapip0  41383  hgmapvv  41394  aks6d1c4  41590  cmpfiiin  42108  pellexlem4  42243  pellqrex  42290  acongtr  42390  acongrep  42392  jm2.23  42408  omlimcl2  42661  onsucf1lem  42689  oege1  42726  nnoeomeqom  42732  cantnfresb  42744  onmcl  42751  tfsconcat0i  42765  ofoafg  42774  ofoafo  42776  ofoaass  42780  ofoacom  42781  naddcnfass  42789  rp-fakeanorass  42934  rp-isfinite6  42939  harval3  42959  inintabss  42999  rfovcnvf1od  43425  clsk1indlem3  43464  ntrclsk13  43492  pm10.55  43797  refsum2cnlem1  44390  axccd2  44594  mptssid  44607  fmuldfeq  44962  climsuse  44987  limclner  45030  climxlim2lem  45224  icccncfext  45266  stoweidlem26  45405  stoweidlem52  45431  stoweidlem57  45436  fourierdlem20  45506  fourierdlem41  45527  fourierdlem52  45537  fourierdlem64  45549  fourierdlem102  45587  fourierdlem114  45599  ovolval4lem1  46028  preimagelt  46078  preimalegt  46079  funressneu  46420  afvelrn  46539  elfz2z  46686  2ffzoeq  46699  imasetpreimafvbijlemfv  46733  imasetpreimafvbijlemf1  46735  fargshiftfva  46774  ichreuopeq  46804  2exopprim  46856  reuopreuprim  46857  fmtnoprmfac1  46896  proththd  46945  opoeALTV  47014  evensumeven  47038  sbgoldbalt  47112  evengpop3  47129  evengpoap3  47130  nnsum4primeseven  47131  nnsum4primesevenALTV  47132  wtgoldbnnsum4prm  47133  bgoldbnnsum3prm  47135  tgoldbach  47148  uspgrimprop  47162  isuspgrimlem  47163  gricushgr  47174  assintop  47262  uzlidlring  47288  2zrngnmrid  47309  cznrng  47314  lmodvsmdi  47437  lincsum  47488  lincsumcl  47490  el0ldep  47525  ldepspr  47532  lindssnlvec  47545  modn0mul  47584  m1modmmod  47585  nn0digval  47664  1arympt1fv  47703  eenglngeehlnmlem1  47801  rrx2linest  47806  line2  47816  itsclc0yqe  47825  r19.41dv  47865  setrec1lem3  48111  aacllem  48225