Theorem anim1i 618

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  sylanl1  680  sylanr1  682  eu6im  2574  r19.28v  3108  rmob  3802  eqeuel  4277  preq12nebg  4773  fores  6643  ssimaex  6796  dffv2  6806  exfo  6924  fpropnf1  7079  oprabv  7271  ndmovass  7396  fun11uni  7710  fabexg  7712  f1oabexg  7714  f1iun  7717  soxp  7896  tz7.48lem  8177  tz7.49c  8182  omass  8308  oewordri  8320  omabs  8376  sbthlem9  8764  pssnn  8846  fineqvlem  8892  pssnnOLD  8895  domunfican  8944  fiint  8948  fsuppsssupp  9001  sup0  9082  inf1  9237  infeq5  9252  cantnfle  9286  rankuni  9479  djuunxp  9537  acndom  9665  acnnum  9666  cdainflem  9801  cfcof  9888  ac6num  10093  ac6s2  10100  brdom5  10143  brdom4  10144  genpnnp  10619  divmulasscom  11514  lediv2a  11726  supmul1  11801  infregelb  11816  nn2ge  11857  btwnz  12279  eluz2b2  12517  uz2mulcl  12522  eqreznegel  12530  xrsupexmnf  12895  xrinfmexpnf  12896  xrsupsslem  12897  xrinfmsslem  12898  supxrun  12906  ioo0  12960  elioo4g  12995  fz0fzelfz0  13218  fz0fzdiffz0  13221  2ffzeq  13233  elfzodifsumelfzo  13308  elfzom1elp1fzo  13309  zpnn0elfzo  13315  elfzom1elp1fzo1  13342  fzonfzoufzol  13345  quoremnn0  13429  zmodidfzoimp  13474  modabs  13477  modmuladd  13486  modifeq2int  13506  modaddmulmod  13511  expcl2lem  13647  hashgt23el  13991  hashreshashfun  14006  iswrdsymb  14086  ccatcl  14129  ccatsymb  14139  swrdfv2  14226  swrdsbslen  14229  swrdspsleq  14230  pfxswrd  14271  pfxccatin12lem3  14297  pfxccatpfx2  14302  swrdccat3blem  14304  reuccatpfxs1  14312  repswccat  14351  cshweqdifid  14385  lswco  14404  repsco  14405  s4f1o  14483  ccat2s1fvwALTOLD  14522  trclun  14577  mulre  14684  rediv  14694  imdiv  14701  resqrex  14814  caurcvg2  15241  fsumdifsnconst  15355  modfsummods  15357  tanval  15689  p1modz1  15822  negdvdsb  15834  muldvds1  15842  muldvds2  15843  dvdscmulr  15846  dvdsmulcr  15847  sumodd  15949  divalglem8  15961  divgcdnn  16074  lcmfunsnlem2lem2  16196  lcmfun  16202  2mulprm  16250  maxprmfct  16266  vfermltlALT  16355  modprm0  16358  pcpremul  16396  pcmul  16404  oddprmdvds  16456  prmdvdsprmo  16595  cshwsidrepsw  16647  gsumccat  18268  grpissubg  18563  gsmsymgreqlem2  18823  symgfixfo  18831  fsfnn0gsumfsffz  19368  irredn0  19721  gim0to0  19762  lsppratlem1  20184  dvdsrzring  20448  mpofrlmd  20739  matinvgcell  21332  mat1dimcrng  21374  dmatscmcl  21400  scmatscm  21410  scmatghm  21430  scmatmhm  21431  ma1repvcl  21467  slesolinv  21577  slesolinvbi  21578  cramerimplem1  21580  cramerimp  21583  cramerlem1  21584  cramer  21588  cpmatacl  21613  cpmatmcl  21616  mat2pmatghm  21627  mat2pmatmul  21628  m2pmfzgsumcl  21645  decpmatmul  21669  decpmatmulsumfsupp  21670  pmatcollpwfi  21679  pm2mpf1  21696  pm2mpghm  21713  pm2mpmhmlem1  21715  monmat2matmon  21721  chpdmatlem2  21736  chpdmat  21738  cpmadugsumlemB  21771  cpmadugsumlemC  21772  cpmadugsumlemF  21773  clscld  21944  neiptopnei  22029  2ndcdisj2  22354  comppfsc  22429  tx1stc  22547  opnfbas  22739  fbasfip  22765  alexsublem  22941  alexsubALTlem4  22947  cnextcn  22964  ngpocelbl  23602  cphipval  24140  bcthlem5  24225  vitalilem4  24508  vitalilem5  24509  itg2mulc  24645  bddiblnc  24739  dvcobr  24843  dvcnvlem  24873  dvferm1  24882  dvne0  24908  mdegmullem  24976  plyeq0lem  25104  plyexmo  25206  aalioulem5  25229  aalioulem6  25230  aaliou  25231  cxple2a  25587  cxpaddlelem  25637  cxpaddle  25638  relogbcxpb  25670  bcmono  26158  lgsprme0  26220  gausslemma2dlem0e  26241  gausslemma2dlem1a  26246  gausslemma2dlem6  26253  lgsquadlem2  26262  2lgsoddprm  26297  colinearalg  27001  axcontlem3  27057  umgrislfupgrlem  27213  edgupgr  27225  usgruspgrb  27272  usgrislfuspgr  27275  edgssv2  27286  umgr2edg  27297  uspgredg2v  27312  usgrexmplef  27347  subupgr  27375  subusgr  27377  nbupgrres  27452  nb3gr2nb  27472  nbupgruvtxres  27495  cusgrres  27536  cusgrsizeindslem  27539  cusgrsizeinds  27540  vtxdun  27569  finrusgrfusgr  27653  cusgrrusgr  27669  spthdep  27821  cycliscrct  27886  crctcshwlkn0lem6  27899  crctcshwlkn0lem7  27900  crctcshtrl  27907  crctcsh  27908  umgr2adedgwlkonALT  28031  elwwlks2  28050  elwspths2spth  28051  rusgrnumwwlk  28059  clwlkclwwlklem2a  28081  clwlkclwwlklem3  28084  clwwisshclwws  28098  wwlksubclwwlk  28141  eleclclwwlknlem2  28144  eupth2lem3lem3  28313  eucrct2eupth1  28327  frgr3v  28358  3vfriswmgr  28361  1to3vfriswmgr  28363  3cyclfrgr  28371  vdgn1frgrv2  28379  frgrwopreglem5  28404  frgrwopreglem5ALT  28405  frrusgrord0lem  28422  frrusgrord0  28423  2clwwlk2clwwlk  28433  extwwlkfab  28435  numclwwlk1lem2fo  28441  friendshipgt3  28481  ex-natded9.20-2  28501  grpoidinvlem3  28587  grpoidinv  28589  nmobndseqi  28860  nmobndseqiALT  28861  hvaddsub4  29159  ocsh  29364  5oalem2  29736  5oalem5  29739  3oalem2  29744  pjjsi  29781  hoadddir  29885  leopmul  30215  stge1i  30319  hatomistici  30443  mdsymlem2  30485  mdsymlem5  30488  addltmulALT  30527  isoun  30754  fsumiunle  30863  lsmsnorb  31293  crefdf  31512  qqhre  31682  esumiun  31774  sxbrsigalem0  31950  dya2iocnei  31961  sxbrsigalem5  31967  sibfinima  32018  eulerpartlemgs2  32059  ballotlemfc0  32171  ballotlemfcc  32172  ballotlemsup  32183  bnj529  32433  bnj945  32466  bnj1098  32476  bnj1533  32545  bnj605  32600  bnj594  32605  bnj607  32609  bnj966  32637  bnj967  32638  bnj996  32649  bnj999  32651  bnj1006  32653  bnj1118  32677  bnj1172  32694  bnj1279  32711  bnj1296  32714  bnj1498  32754  fnrelpredd  32774  lfuhgr3  32794  loop1cycl  32812  cvmsi  32940  satf0op  33052  satffunlem1lem1  33077  satffunlem2lem1  33079  fv2ndcnv  33471  elno2  33594  cofcutr  33829  trisegint  34067  funtransport  34070  btwnconn1lem4  34129  btwnconn2  34141  segcon2  34144  outsideofeu  34170  isfne  34265  lukshef-ax2  34341  limsucncmpi  34371  bj-nsnid  34977  bj-restn0b  34997  bj-eldiag2  35083  bj-isrvec2  35205  pibt2  35325  unccur  35497  lindsadd  35507  lindsenlbs  35509  matunitlindflem1  35510  matunitlindflem2  35511  poimirlem26  35540  poimirlem27  35541  poimirlem29  35543  poimirlem30  35544  poimirlem32  35546  heicant  35549  ismblfin  35555  itg2gt0cn  35569  areacirc  35607  opelopab3  35612  isdivrngo  35845  isdrngo2  35853  fldcrng  35899  flddmn  35953  refrelredund4  36485  cmtbr4N  37006  linepsubN  37503  pmapsub  37519  paddasslem14  37584  pclcmpatN  37652  trlval2  37914  cdleme20  38075  cdleme21j  38087  dvalveclem  38776  dia2dimlem7  38821  dvhlveclem  38859  docaclN  38875  dihjat1  39180  mapdhcl  39478  mapdh6dN  39490  mapdh8  39539  hdmap1l6d  39564  hdmap10  39591  hdmaprnlem17N  39614  hdmaplkr  39664  hdmapip0  39666  hgmapvv  39677  cmpfiiin  40222  pellexlem4  40357  pellqrex  40404  acongtr  40503  acongrep  40505  jm2.23  40521  rp-fakeanorass  40805  rp-isfinite6  40810  harval3  40828  inintabss  40862  rfovcnvf1od  41289  clsk1indlem3  41330  ntrclsk13  41358  pm10.55  41660  refsum2cnlem1  42253  axccd2  42442  mptssid  42457  fmuldfeq  42799  climsuse  42824  limclner  42867  climxlim2lem  43061  icccncfext  43103  stoweidlem26  43242  stoweidlem52  43268  stoweidlem57  43273  fourierdlem20  43343  fourierdlem41  43364  fourierdlem52  43374  fourierdlem64  43386  fourierdlem102  43424  fourierdlem114  43436  ovolval4lem1  43862  preimagelt  43911  preimalegt  43912  funressneu  44213  afvelrn  44332  elfz2z  44480  2ffzoeq  44493  imasetpreimafvbijlemfv  44527  imasetpreimafvbijlemf1  44529  fargshiftfva  44568  ichreuopeq  44598  2exopprim  44650  reuopreuprim  44651  fmtnoprmfac1  44690  proththd  44739  opoeALTV  44808  evensumeven  44832  sbgoldbalt  44906  evengpop3  44923  evengpoap3  44924  nnsum4primeseven  44925  nnsum4primesevenALTV  44926  wtgoldbnnsum4prm  44927  bgoldbnnsum3prm  44929  tgoldbach  44942  isomushgr  44951  assintop  45076  isringrng  45112  rnglz  45115  c0snmgmhm  45145  zrrnghm  45148  uzlidlring  45160  2zrngnmrid  45181  cznrng  45186  rnghmsubcsetclem2  45207  rhmsubcsetclem2  45253  rhmsubcrngclem2  45259  lmodvsmdi  45391  lincsum  45443  lincsumcl  45445  el0ldep  45480  ldepspr  45487  lindssnlvec  45500  modn0mul  45539  m1modmmod  45540  nn0digval  45619  1arympt1fv  45658  eenglngeehlnmlem1  45756  rrx2linest  45761  line2  45771  itsclc0yqe  45780  r19.41dv  45820  setrec1lem3  46066  aacllem  46176