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  677  sylanr1  679  eu6im  2568  r19.28v  3188  rmob  3884  eqeuel  4362  preq12nebg  4863  fores  6815  ssimaex  6976  dffv2  6986  exfo  7106  fpropnf1  7269  oprabv  7472  ndmovass  7599  fun11uni  7927  fabexg  7929  f1oabexg  7931  f1iun  7934  soxp  8120  tz7.48lem  8447  tz7.49c  8452  omass  8586  oewordri  8598  omabs  8656  sbthlem9  9097  pssnn  9174  fineqvlem  9268  pssnnOLD  9271  domunfican  9326  fiint  9330  fsuppsssupp  9385  sup0  9467  inf1  9623  infeq5  9638  cantnfle  9672  rankuni  9864  djuunxp  9922  acndom  10052  acnnum  10053  cdainflem  10188  cfcof  10275  ac6num  10480  ac6s2  10487  brdom5  10530  brdom4  10531  genpnnp  11006  divmulasscom  11903  lediv2a  12115  supmul1  12190  infregelb  12205  nn2ge  12246  btwnz  12672  eluz2b2  12912  uz2mulcl  12917  eqreznegel  12925  xrsupexmnf  13291  xrinfmexpnf  13292  xrsupsslem  13293  xrinfmsslem  13294  supxrun  13302  ioo0  13356  elioo4g  13391  fz0fzelfz0  13614  fz0fzdiffz0  13617  2ffzeq  13629  elfzodifsumelfzo  13705  elfzom1elp1fzo  13706  zpnn0elfzo  13712  elfzom1elp1fzo1  13739  fzonfzoufzol  13742  quoremnn0  13828  zmodidfzoimp  13873  modabs  13876  modmuladd  13885  modifeq2int  13905  modaddmulmod  13910  expcl2lem  14046  hashgt23el  14391  hashreshashfun  14406  iswrdsymb  14488  ccatcl  14531  ccatsymb  14539  swrdfv2  14618  swrdsbslen  14621  swrdspsleq  14622  pfxswrd  14663  pfxccatin12lem3  14689  pfxccatpfx2  14694  swrdccat3blem  14696  reuccatpfxs1  14704  repswccat  14743  cshweqdifid  14777  lswco  14797  repsco  14798  s4f1o  14876  trclun  14968  mulre  15075  rediv  15085  imdiv  15092  resqrex  15204  caurcvg2  15631  fsumdifsnconst  15744  modfsummods  15746  tanval  16078  p1modz1  16211  negdvdsb  16223  muldvds1  16231  muldvds2  16232  dvdscmulr  16235  dvdsmulcr  16236  sumodd  16338  divalglem8  16350  divgcdnn  16463  lcmfunsnlem2lem2  16583  lcmfun  16589  2mulprm  16637  maxprmfct  16653  vfermltlALT  16742  modprm0  16745  pcpremul  16783  pcmul  16791  oddprmdvds  16843  prmdvdsprmo  16982  cshwsidrepsw  17034  gsumccat  18764  grpissubg  19069  ecqusaddd  19114  ecqusaddcl  19115  eqg0subg  19118  gim0to0  19190  gsmsymgreqlem2  19347  symgfixfo  19355  fsfnn0gsumfsffz  19899  rnglz  20066  isringrng  20182  irredn0  20321  c0snmgmhm  20360  rimisrngim  20396  zrrnghm  20432  rnghmsubcsetclem2  20524  rhmsubcsetclem2  20553  rhmsubcrngclem2  20559  lsppratlem1  20994  qusmulrng  21117  quscrng  21118  rngqiprngghmlem3  21137  rngqiprnglinlem3  21141  rngqiprngimf1lem  21142  rngqiprnglin  21150  cnfldfunALT  21246  dvdsrzring  21321  mpofrlmd  21642  matinvgcell  22257  mat1dimcrng  22299  dmatscmcl  22325  scmatscm  22335  scmatghm  22355  scmatmhm  22356  ma1repvcl  22392  slesolinv  22502  slesolinvbi  22503  cramerimplem1  22505  cramerimp  22508  cramerlem1  22509  cramer  22513  cpmatacl  22538  cpmatmcl  22541  mat2pmatghm  22552  mat2pmatmul  22553  m2pmfzgsumcl  22570  decpmatmul  22594  decpmatmulsumfsupp  22595  pmatcollpwfi  22604  pm2mpf1  22621  pm2mpghm  22638  pm2mpmhmlem1  22640  monmat2matmon  22646  chpdmatlem2  22661  chpdmat  22663  cpmadugsumlemB  22696  cpmadugsumlemC  22697  cpmadugsumlemF  22698  clscld  22871  neiptopnei  22956  2ndcdisj2  23281  comppfsc  23356  tx1stc  23474  opnfbas  23666  fbasfip  23692  alexsublem  23868  alexsubALTlem4  23874  cnextcn  23891  ngpocelbl  24541  cphipval  25091  bcthlem5  25176  vitalilem4  25460  vitalilem5  25461  itg2mulc  25597  bddiblnc  25691  dvcobr  25797  dvcobrOLD  25798  dvcnvlem  25828  dvferm1  25837  dvne0  25864  mdegmullem  25934  plyeq0lem  26062  plyexmo  26165  aalioulem5  26188  aalioulem6  26189  aaliou  26190  cxple2a  26547  cxpaddlelem  26600  cxpaddle  26601  relogbcxpb  26633  bcmono  27123  lgsprme0  27185  gausslemma2dlem0e  27206  gausslemma2dlem1a  27211  gausslemma2dlem6  27218  lgsquadlem2  27227  2lgsoddprm  27262  elno2  27500  cofcutr  27757  colinearalg  28601  axcontlem3  28657  umgrislfupgrlem  28815  edgupgr  28827  usgruspgrb  28874  usgrislfuspgr  28877  edgssv2  28888  umgr2edg  28899  uspgredg2v  28914  usgrexmplef  28949  subupgr  28977  subusgr  28979  nbupgrres  29054  nb3gr2nb  29074  nbupgruvtxres  29097  cusgrres  29138  cusgrsizeindslem  29141  cusgrsizeinds  29142  vtxdun  29171  finrusgrfusgr  29255  cusgrrusgr  29271  spthdep  29424  cycliscrct  29489  crctcshwlkn0lem6  29502  crctcshwlkn0lem7  29503  crctcshtrl  29510  crctcsh  29511  umgr2adedgwlkonALT  29634  elwwlks2  29653  elwspths2spth  29654  rusgrnumwwlk  29662  clwlkclwwlklem2a  29684  clwlkclwwlklem3  29687  clwwisshclwws  29701  wwlksubclwwlk  29744  eleclclwwlknlem2  29747  eupth2lem3lem3  29916  eucrct2eupth1  29930  frgr3v  29961  3vfriswmgr  29964  1to3vfriswmgr  29966  3cyclfrgr  29974  vdgn1frgrv2  29982  frgrwopreglem5  30007  frgrwopreglem5ALT  30008  frrusgrord0lem  30025  frrusgrord0  30026  2clwwlk2clwwlk  30036  extwwlkfab  30038  numclwwlk1lem2fo  30044  friendshipgt3  30084  ex-natded9.20-2  30104  grpoidinvlem3  30192  grpoidinv  30194  nmobndseqi  30465  nmobndseqiALT  30466  hvaddsub4  30764  ocsh  30969  5oalem2  31341  5oalem5  31344  3oalem2  31349  pjjsi  31386  hoadddir  31490  leopmul  31820  stge1i  31924  hatomistici  32048  mdsymlem2  32090  mdsymlem5  32093  addltmulALT  32132  isoun  32356  fsumiunle  32468  lsmsnorb  32941  crefdf  33292  qqhre  33464  esumiun  33556  sxbrsigalem0  33734  dya2iocnei  33745  sxbrsigalem5  33751  sibfinima  33802  eulerpartlemgs2  33843  ballotlemfc0  33955  ballotlemfcc  33956  ballotlemsup  33967  bnj529  34216  bnj945  34248  bnj1098  34258  bnj1533  34327  bnj605  34382  bnj594  34387  bnj607  34391  bnj966  34419  bnj967  34420  bnj996  34431  bnj999  34433  bnj1006  34435  bnj1118  34459  bnj1172  34476  bnj1279  34493  bnj1296  34496  bnj1498  34536  fnrelpredd  34556  lfuhgr3  34574  loop1cycl  34592  cvmsi  34720  satf0op  34832  satffunlem1lem1  34857  satffunlem2lem1  34859  fv2ndcnv  35219  trisegint  35470  funtransport  35473  btwnconn1lem4  35532  btwnconn2  35544  segcon2  35547  outsideofeu  35573  gg-cnfldfunALT  35645  isfne  35688  lukshef-ax2  35764  limsucncmpi  35794  bj-nsnid  36415  bj-restn0b  36436  bj-eldiag2  36522  bj-isrvec2  36645  pibt2  36762  unccur  36935  lindsadd  36945  lindsenlbs  36947  matunitlindflem1  36948  matunitlindflem2  36949  poimirlem26  36978  poimirlem27  36979  poimirlem29  36981  poimirlem30  36982  poimirlem32  36984  heicant  36987  ismblfin  36993  itg2gt0cn  37007  areacirc  37045  opelopab3  37050  isdivrngo  37282  isdrngo2  37290  fldcrngo  37336  flddmn  37390  refrelredund4  37969  mainer2  38180  cmtbr4N  38589  linepsubN  39087  pmapsub  39103  paddasslem14  39168  pclcmpatN  39236  trlval2  39498  cdleme20  39659  cdleme21j  39671  dvalveclem  40360  dia2dimlem7  40405  dvhlveclem  40443  docaclN  40459  dihjat1  40764  mapdhcl  41062  mapdh6dN  41074  mapdh8  41123  hdmap1l6d  41148  hdmap10  41175  hdmaprnlem17N  41198  hdmaplkr  41248  hdmapip0  41250  hgmapvv  41261  cmpfiiin  41898  pellexlem4  42033  pellqrex  42080  acongtr  42180  acongrep  42182  jm2.23  42198  omlimcl2  42454  onsucf1lem  42482  oege1  42519  nnoeomeqom  42525  cantnfresb  42537  onmcl  42544  tfsconcat0i  42558  ofoafg  42567  ofoafo  42569  ofoaass  42573  ofoacom  42574  naddcnfass  42582  rp-fakeanorass  42727  rp-isfinite6  42732  harval3  42752  inintabss  42792  rfovcnvf1od  43218  clsk1indlem3  43257  ntrclsk13  43285  pm10.55  43591  refsum2cnlem1  44184  axccd2  44388  mptssid  44403  fmuldfeq  44758  climsuse  44783  limclner  44826  climxlim2lem  45020  icccncfext  45062  stoweidlem26  45201  stoweidlem52  45227  stoweidlem57  45232  fourierdlem20  45302  fourierdlem41  45323  fourierdlem52  45333  fourierdlem64  45345  fourierdlem102  45383  fourierdlem114  45395  ovolval4lem1  45824  preimagelt  45874  preimalegt  45875  funressneu  46216  afvelrn  46335  elfz2z  46482  2ffzoeq  46495  imasetpreimafvbijlemfv  46529  imasetpreimafvbijlemf1  46531  fargshiftfva  46570  ichreuopeq  46600  2exopprim  46652  reuopreuprim  46653  fmtnoprmfac1  46692  proththd  46741  opoeALTV  46810  evensumeven  46834  sbgoldbalt  46908  evengpop3  46925  evengpoap3  46926  nnsum4primeseven  46927  nnsum4primesevenALTV  46928  wtgoldbnnsum4prm  46929  bgoldbnnsum3prm  46931  tgoldbach  46944  isomushgr  46953  assintop  47046  uzlidlring  47072  2zrngnmrid  47093  cznrng  47098  lmodvsmdi  47221  lincsum  47272  lincsumcl  47274  el0ldep  47309  ldepspr  47316  lindssnlvec  47329  modn0mul  47368  m1modmmod  47369  nn0digval  47448  1arympt1fv  47487  eenglngeehlnmlem1  47585  rrx2linest  47590  line2  47600  itsclc0yqe  47609  r19.41dv  47649  setrec1lem3  47896  aacllem  48010