Theorem anim1i 616

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 614	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  sylanl1  679  sylanr1  681  eu6im  2570  r19.28v  3190  rmob  3884  eqeuel  4362  preq12nebg  4863  fores  6813  ssimaex  6974  dffv2  6984  exfo  7104  fpropnf1  7263  oprabv  7466  ndmovass  7592  fun11uni  7920  fabexg  7922  f1oabexg  7924  f1iun  7927  soxp  8112  tz7.48lem  8438  tz7.49c  8443  omass  8577  oewordri  8589  omabs  8647  sbthlem9  9088  pssnn  9165  fineqvlem  9259  pssnnOLD  9262  domunfican  9317  fiint  9321  fsuppsssupp  9376  sup0  9458  inf1  9614  infeq5  9629  cantnfle  9663  rankuni  9855  djuunxp  9913  acndom  10043  acnnum  10044  cdainflem  10179  cfcof  10266  ac6num  10471  ac6s2  10478  brdom5  10521  brdom4  10522  genpnnp  10997  divmulasscom  11893  lediv2a  12105  supmul1  12180  infregelb  12195  nn2ge  12236  btwnz  12662  eluz2b2  12902  uz2mulcl  12907  eqreznegel  12915  xrsupexmnf  13281  xrinfmexpnf  13282  xrsupsslem  13283  xrinfmsslem  13284  supxrun  13292  ioo0  13346  elioo4g  13381  fz0fzelfz0  13604  fz0fzdiffz0  13607  2ffzeq  13619  elfzodifsumelfzo  13695  elfzom1elp1fzo  13696  zpnn0elfzo  13702  elfzom1elp1fzo1  13729  fzonfzoufzol  13732  quoremnn0  13818  zmodidfzoimp  13863  modabs  13866  modmuladd  13875  modifeq2int  13895  modaddmulmod  13900  expcl2lem  14036  hashgt23el  14381  hashreshashfun  14396  iswrdsymb  14478  ccatcl  14521  ccatsymb  14529  swrdfv2  14608  swrdsbslen  14611  swrdspsleq  14612  pfxswrd  14653  pfxccatin12lem3  14679  pfxccatpfx2  14684  swrdccat3blem  14686  reuccatpfxs1  14694  repswccat  14733  cshweqdifid  14767  lswco  14787  repsco  14788  s4f1o  14866  trclun  14958  mulre  15065  rediv  15075  imdiv  15082  resqrex  15194  caurcvg2  15621  fsumdifsnconst  15734  modfsummods  15736  tanval  16068  p1modz1  16201  negdvdsb  16213  muldvds1  16221  muldvds2  16222  dvdscmulr  16225  dvdsmulcr  16226  sumodd  16328  divalglem8  16340  divgcdnn  16453  lcmfunsnlem2lem2  16573  lcmfun  16579  2mulprm  16627  maxprmfct  16643  vfermltlALT  16732  modprm0  16735  pcpremul  16773  pcmul  16781  oddprmdvds  16833  prmdvdsprmo  16972  cshwsidrepsw  17024  gsumccat  18719  grpissubg  19021  eqg0subg  19068  gsmsymgreqlem2  19294  symgfixfo  19302  fsfnn0gsumfsffz  19846  irredn0  20230  gim0to0  20274  lsppratlem1  20753  cnfldfunALT  20950  dvdsrzring  21023  mpofrlmd  21324  matinvgcell  21929  mat1dimcrng  21971  dmatscmcl  21997  scmatscm  22007  scmatghm  22027  scmatmhm  22028  ma1repvcl  22064  slesolinv  22174  slesolinvbi  22175  cramerimplem1  22177  cramerimp  22180  cramerlem1  22181  cramer  22185  cpmatacl  22210  cpmatmcl  22213  mat2pmatghm  22224  mat2pmatmul  22225  m2pmfzgsumcl  22242  decpmatmul  22266  decpmatmulsumfsupp  22267  pmatcollpwfi  22276  pm2mpf1  22293  pm2mpghm  22310  pm2mpmhmlem1  22312  monmat2matmon  22318  chpdmatlem2  22333  chpdmat  22335  cpmadugsumlemB  22368  cpmadugsumlemC  22369  cpmadugsumlemF  22370  clscld  22543  neiptopnei  22628  2ndcdisj2  22953  comppfsc  23028  tx1stc  23146  opnfbas  23338  fbasfip  23364  alexsublem  23540  alexsubALTlem4  23546  cnextcn  23563  ngpocelbl  24213  cphipval  24752  bcthlem5  24837  vitalilem4  25120  vitalilem5  25121  itg2mulc  25257  bddiblnc  25351  dvcobr  25455  dvcnvlem  25485  dvferm1  25494  dvne0  25520  mdegmullem  25588  plyeq0lem  25716  plyexmo  25818  aalioulem5  25841  aalioulem6  25842  aaliou  25843  cxple2a  26199  cxpaddlelem  26249  cxpaddle  26250  relogbcxpb  26282  bcmono  26770  lgsprme0  26832  gausslemma2dlem0e  26853  gausslemma2dlem1a  26858  gausslemma2dlem6  26865  lgsquadlem2  26874  2lgsoddprm  26909  elno2  27147  cofcutr  27401  colinearalg  28158  axcontlem3  28214  umgrislfupgrlem  28372  edgupgr  28384  usgruspgrb  28431  usgrislfuspgr  28434  edgssv2  28445  umgr2edg  28456  uspgredg2v  28471  usgrexmplef  28506  subupgr  28534  subusgr  28536  nbupgrres  28611  nb3gr2nb  28631  nbupgruvtxres  28654  cusgrres  28695  cusgrsizeindslem  28698  cusgrsizeinds  28699  vtxdun  28728  finrusgrfusgr  28812  cusgrrusgr  28828  spthdep  28981  cycliscrct  29046  crctcshwlkn0lem6  29059  crctcshwlkn0lem7  29060  crctcshtrl  29067  crctcsh  29068  umgr2adedgwlkonALT  29191  elwwlks2  29210  elwspths2spth  29211  rusgrnumwwlk  29219  clwlkclwwlklem2a  29241  clwlkclwwlklem3  29244  clwwisshclwws  29258  wwlksubclwwlk  29301  eleclclwwlknlem2  29304  eupth2lem3lem3  29473  eucrct2eupth1  29487  frgr3v  29518  3vfriswmgr  29521  1to3vfriswmgr  29523  3cyclfrgr  29531  vdgn1frgrv2  29539  frgrwopreglem5  29564  frgrwopreglem5ALT  29565  frrusgrord0lem  29582  frrusgrord0  29583  2clwwlk2clwwlk  29593  extwwlkfab  29595  numclwwlk1lem2fo  29601  friendshipgt3  29641  ex-natded9.20-2  29661  grpoidinvlem3  29747  grpoidinv  29749  nmobndseqi  30020  nmobndseqiALT  30021  hvaddsub4  30319  ocsh  30524  5oalem2  30896  5oalem5  30899  3oalem2  30904  pjjsi  30941  hoadddir  31045  leopmul  31375  stge1i  31479  hatomistici  31603  mdsymlem2  31645  mdsymlem5  31648  addltmulALT  31687  isoun  31911  fsumiunle  32023  lsmsnorb  32490  crefdf  32817  qqhre  32989  esumiun  33081  sxbrsigalem0  33259  dya2iocnei  33270  sxbrsigalem5  33276  sibfinima  33327  eulerpartlemgs2  33368  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemsup  33492  bnj529  33741  bnj945  33773  bnj1098  33783  bnj1533  33852  bnj605  33907  bnj594  33912  bnj607  33916  bnj966  33944  bnj967  33945  bnj996  33956  bnj999  33958  bnj1006  33960  bnj1118  33984  bnj1172  34001  bnj1279  34018  bnj1296  34021  bnj1498  34061  fnrelpredd  34081  lfuhgr3  34099  loop1cycl  34117  cvmsi  34245  satf0op  34357  satffunlem1lem1  34382  satffunlem2lem1  34384  fv2ndcnv  34738  trisegint  34989  funtransport  34992  btwnconn1lem4  35051  btwnconn2  35063  segcon2  35066  outsideofeu  35092  gg-dvcobr  35165  isfne  35213  lukshef-ax2  35289  limsucncmpi  35319  bj-nsnid  35940  bj-restn0b  35961  bj-eldiag2  36047  bj-isrvec2  36170  pibt2  36287  unccur  36460  lindsadd  36470  lindsenlbs  36472  matunitlindflem1  36473  matunitlindflem2  36474  poimirlem26  36503  poimirlem27  36504  poimirlem29  36506  poimirlem30  36507  poimirlem32  36509  heicant  36512  ismblfin  36518  itg2gt0cn  36532  areacirc  36570  opelopab3  36575  isdivrngo  36807  isdrngo2  36815  fldcrngo  36861  flddmn  36915  refrelredund4  37494  mainer2  37705  cmtbr4N  38114  linepsubN  38612  pmapsub  38628  paddasslem14  38693  pclcmpatN  38761  trlval2  39023  cdleme20  39184  cdleme21j  39196  dvalveclem  39885  dia2dimlem7  39930  dvhlveclem  39968  docaclN  39984  dihjat1  40289  mapdhcl  40587  mapdh6dN  40599  mapdh8  40648  hdmap1l6d  40673  hdmap10  40700  hdmaprnlem17N  40723  hdmaplkr  40773  hdmapip0  40775  hgmapvv  40786  cmpfiiin  41421  pellexlem4  41556  pellqrex  41603  acongtr  41703  acongrep  41705  jm2.23  41721  omlimcl2  41977  onsucf1lem  42005  oege1  42042  nnoeomeqom  42048  cantnfresb  42060  onmcl  42067  tfsconcat0i  42081  ofoafg  42090  ofoafo  42092  ofoaass  42096  ofoacom  42097  naddcnfass  42105  rp-fakeanorass  42250  rp-isfinite6  42255  harval3  42275  inintabss  42315  rfovcnvf1od  42741  clsk1indlem3  42780  ntrclsk13  42808  pm10.55  43114  refsum2cnlem1  43707  axccd2  43915  mptssid  43930  fmuldfeq  44286  climsuse  44311  limclner  44354  climxlim2lem  44548  icccncfext  44590  stoweidlem26  44729  stoweidlem52  44755  stoweidlem57  44760  fourierdlem20  44830  fourierdlem41  44851  fourierdlem52  44861  fourierdlem64  44873  fourierdlem102  44911  fourierdlem114  44923  ovolval4lem1  45352  preimagelt  45402  preimalegt  45403  funressneu  45744  afvelrn  45863  elfz2z  46010  2ffzoeq  46023  imasetpreimafvbijlemfv  46057  imasetpreimafvbijlemf1  46059  fargshiftfva  46098  ichreuopeq  46128  2exopprim  46180  reuopreuprim  46181  fmtnoprmfac1  46220  proththd  46269  opoeALTV  46338  evensumeven  46362  sbgoldbalt  46436  evengpop3  46453  evengpoap3  46454  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  wtgoldbnnsum4prm  46457  bgoldbnnsum3prm  46459  tgoldbach  46472  isomushgr  46481  assintop  46606  isringrng  46644  rnglz  46651  c0snmgmhm  46699  zrrnghm  46702  ecqusadd  46750  ecqusaddcl  46751  qusmulrng  46752  rngqiprngghmlem3  46755  rngqiprnglinlem3  46759  rngqiprngimf1lem  46760  rngqiprnglin  46768  uzlidlring  46781  2zrngnmrid  46802  cznrng  46807  rnghmsubcsetclem2  46828  rhmsubcsetclem2  46874  rhmsubcrngclem2  46880  lmodvsmdi  47012  lincsum  47064  lincsumcl  47066  el0ldep  47101  ldepspr  47108  lindssnlvec  47121  modn0mul  47160  m1modmmod  47161  nn0digval  47240  1arympt1fv  47279  eenglngeehlnmlem1  47377  rrx2linest  47382  line2  47392  itsclc0yqe  47401  r19.41dv  47441  setrec1lem3  47688  aacllem  47802