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 396

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 397

This theorem is referenced by:  sylanl1  677  sylanr1  679  eu6im  2573  r19.28v  3182  rmob  3833  eqeuel  4308  preq12nebg  4806  fores  6743  ssimaex  6903  dffv2  6913  exfo  7031  fpropnf1  7190  oprabv  7389  ndmovass  7514  fun11uni  7839  fabexg  7841  f1oabexg  7843  f1iun  7846  soxp  8029  tz7.48lem  8334  tz7.49c  8339  omass  8474  oewordri  8486  omabs  8544  sbthlem9  8948  pssnn  9025  fineqvlem  9119  pssnnOLD  9122  domunfican  9177  fiint  9181  fsuppsssupp  9234  sup0  9315  inf1  9471  infeq5  9486  cantnfle  9520  rankuni  9712  djuunxp  9770  acndom  9900  acnnum  9901  cdainflem  10036  cfcof  10123  ac6num  10328  ac6s2  10335  brdom5  10378  brdom4  10379  genpnnp  10854  divmulasscom  11750  lediv2a  11962  supmul1  12037  infregelb  12052  nn2ge  12093  btwnz  12516  eluz2b2  12754  uz2mulcl  12759  eqreznegel  12767  xrsupexmnf  13132  xrinfmexpnf  13133  xrsupsslem  13134  xrinfmsslem  13135  supxrun  13143  ioo0  13197  elioo4g  13232  fz0fzelfz0  13455  fz0fzdiffz0  13458  2ffzeq  13470  elfzodifsumelfzo  13546  elfzom1elp1fzo  13547  zpnn0elfzo  13553  elfzom1elp1fzo1  13580  fzonfzoufzol  13583  quoremnn0  13669  zmodidfzoimp  13714  modabs  13717  modmuladd  13726  modifeq2int  13746  modaddmulmod  13751  expcl2lem  13887  hashgt23el  14231  hashreshashfun  14246  iswrdsymb  14326  ccatcl  14369  ccatsymb  14378  swrdfv2  14464  swrdsbslen  14467  swrdspsleq  14468  pfxswrd  14509  pfxccatin12lem3  14535  pfxccatpfx2  14540  swrdccat3blem  14542  reuccatpfxs1  14550  repswccat  14589  cshweqdifid  14623  lswco  14643  repsco  14644  s4f1o  14722  ccat2s1fvwALTOLD  14761  trclun  14816  mulre  14923  rediv  14933  imdiv  14940  resqrex  15053  caurcvg2  15480  fsumdifsnconst  15594  modfsummods  15596  tanval  15928  p1modz1  16061  negdvdsb  16073  muldvds1  16081  muldvds2  16082  dvdscmulr  16085  dvdsmulcr  16086  sumodd  16188  divalglem8  16200  divgcdnn  16313  lcmfunsnlem2lem2  16433  lcmfun  16439  2mulprm  16487  maxprmfct  16503  vfermltlALT  16592  modprm0  16595  pcpremul  16633  pcmul  16641  oddprmdvds  16693  prmdvdsprmo  16832  cshwsidrepsw  16884  gsumccat  18568  grpissubg  18863  gsmsymgreqlem2  19127  symgfixfo  19135  fsfnn0gsumfsffz  19671  irredn0  20032  gim0to0  20076  lsppratlem1  20507  cnfldfunALT  20708  dvdsrzring  20781  mpofrlmd  21082  matinvgcell  21682  mat1dimcrng  21724  dmatscmcl  21750  scmatscm  21760  scmatghm  21780  scmatmhm  21781  ma1repvcl  21817  slesolinv  21927  slesolinvbi  21928  cramerimplem1  21930  cramerimp  21933  cramerlem1  21934  cramer  21938  cpmatacl  21963  cpmatmcl  21966  mat2pmatghm  21977  mat2pmatmul  21978  m2pmfzgsumcl  21995  decpmatmul  22019  decpmatmulsumfsupp  22020  pmatcollpwfi  22029  pm2mpf1  22046  pm2mpghm  22063  pm2mpmhmlem1  22065  monmat2matmon  22071  chpdmatlem2  22086  chpdmat  22088  cpmadugsumlemB  22121  cpmadugsumlemC  22122  cpmadugsumlemF  22123  clscld  22296  neiptopnei  22381  2ndcdisj2  22706  comppfsc  22781  tx1stc  22899  opnfbas  23091  fbasfip  23117  alexsublem  23293  alexsubALTlem4  23299  cnextcn  23316  ngpocelbl  23966  cphipval  24505  bcthlem5  24590  vitalilem4  24873  vitalilem5  24874  itg2mulc  25010  bddiblnc  25104  dvcobr  25208  dvcnvlem  25238  dvferm1  25247  dvne0  25273  mdegmullem  25341  plyeq0lem  25469  plyexmo  25571  aalioulem5  25594  aalioulem6  25595  aaliou  25596  cxple2a  25952  cxpaddlelem  26002  cxpaddle  26003  relogbcxpb  26035  bcmono  26523  lgsprme0  26585  gausslemma2dlem0e  26606  gausslemma2dlem1a  26611  gausslemma2dlem6  26618  lgsquadlem2  26627  2lgsoddprm  26662  elno2  26900  colinearalg  27480  axcontlem3  27536  umgrislfupgrlem  27694  edgupgr  27706  usgruspgrb  27753  usgrislfuspgr  27756  edgssv2  27767  umgr2edg  27778  uspgredg2v  27793  usgrexmplef  27828  subupgr  27856  subusgr  27858  nbupgrres  27933  nb3gr2nb  27953  nbupgruvtxres  27976  cusgrres  28017  cusgrsizeindslem  28020  cusgrsizeinds  28021  vtxdun  28050  finrusgrfusgr  28134  cusgrrusgr  28150  spthdep  28303  cycliscrct  28368  crctcshwlkn0lem6  28381  crctcshwlkn0lem7  28382  crctcshtrl  28389  crctcsh  28390  umgr2adedgwlkonALT  28513  elwwlks2  28532  elwspths2spth  28533  rusgrnumwwlk  28541  clwlkclwwlklem2a  28563  clwlkclwwlklem3  28566  clwwisshclwws  28580  wwlksubclwwlk  28623  eleclclwwlknlem2  28626  eupth2lem3lem3  28795  eucrct2eupth1  28809  frgr3v  28840  3vfriswmgr  28843  1to3vfriswmgr  28845  3cyclfrgr  28853  vdgn1frgrv2  28861  frgrwopreglem5  28886  frgrwopreglem5ALT  28887  frrusgrord0lem  28904  frrusgrord0  28905  2clwwlk2clwwlk  28915  extwwlkfab  28917  numclwwlk1lem2fo  28923  friendshipgt3  28963  ex-natded9.20-2  28983  grpoidinvlem3  29069  grpoidinv  29071  nmobndseqi  29342  nmobndseqiALT  29343  hvaddsub4  29641  ocsh  29846  5oalem2  30218  5oalem5  30221  3oalem2  30226  pjjsi  30263  hoadddir  30367  leopmul  30697  stge1i  30801  hatomistici  30925  mdsymlem2  30967  mdsymlem5  30970  addltmulALT  31009  isoun  31234  fsumiunle  31343  lsmsnorb  31789  crefdf  32009  qqhre  32181  esumiun  32273  sxbrsigalem0  32451  dya2iocnei  32462  sxbrsigalem5  32468  sibfinima  32519  eulerpartlemgs2  32560  ballotlemfc0  32672  ballotlemfcc  32673  ballotlemsup  32684  bnj529  32933  bnj945  32965  bnj1098  32975  bnj1533  33044  bnj605  33099  bnj594  33104  bnj607  33108  bnj966  33136  bnj967  33137  bnj996  33148  bnj999  33150  bnj1006  33152  bnj1118  33176  bnj1172  33193  bnj1279  33210  bnj1296  33213  bnj1498  33253  fnrelpredd  33273  lfuhgr3  33293  loop1cycl  33311  cvmsi  33439  satf0op  33551  satffunlem1lem1  33576  satffunlem2lem1  33578  fv2ndcnv  33951  cofcutr  34183  trisegint  34421  funtransport  34424  btwnconn1lem4  34483  btwnconn2  34495  segcon2  34498  outsideofeu  34524  isfne  34619  lukshef-ax2  34695  limsucncmpi  34725  bj-nsnid  35339  bj-restn0b  35360  bj-eldiag2  35446  bj-isrvec2  35569  pibt2  35686  unccur  35858  lindsadd  35868  lindsenlbs  35870  matunitlindflem1  35871  matunitlindflem2  35872  poimirlem26  35901  poimirlem27  35902  poimirlem29  35904  poimirlem30  35905  poimirlem32  35907  heicant  35910  ismblfin  35916  itg2gt0cn  35930  areacirc  35968  opelopab3  35973  isdivrngo  36206  isdrngo2  36214  fldcrngo  36260  flddmn  36314  refrelredund4  36895  mainer2  37106  cmtbr4N  37515  linepsubN  38013  pmapsub  38029  paddasslem14  38094  pclcmpatN  38162  trlval2  38424  cdleme20  38585  cdleme21j  38597  dvalveclem  39286  dia2dimlem7  39331  dvhlveclem  39369  docaclN  39385  dihjat1  39690  mapdhcl  39988  mapdh6dN  40000  mapdh8  40049  hdmap1l6d  40074  hdmap10  40101  hdmaprnlem17N  40124  hdmaplkr  40174  hdmapip0  40176  hgmapvv  40187  cmpfiiin  40769  pellexlem4  40904  pellqrex  40951  acongtr  41051  acongrep  41053  jm2.23  41069  omlimcl2  41299  ofoafg  41308  ofoafo  41310  ofoaass  41314  ofoacom  41315  naddcnfass  41323  rp-fakeanorass  41430  rp-isfinite6  41435  harval3  41455  inintabss  41496  rfovcnvf1od  41922  clsk1indlem3  41963  ntrclsk13  41991  pm10.55  42297  refsum2cnlem1  42890  axccd2  43086  mptssid  43102  fmuldfeq  43449  climsuse  43474  limclner  43517  climxlim2lem  43711  icccncfext  43753  stoweidlem26  43892  stoweidlem52  43918  stoweidlem57  43923  fourierdlem20  43993  fourierdlem41  44014  fourierdlem52  44024  fourierdlem64  44036  fourierdlem102  44074  fourierdlem114  44086  ovolval4lem1  44513  preimagelt  44563  preimalegt  44564  funressneu  44881  afvelrn  45000  elfz2z  45147  2ffzoeq  45160  imasetpreimafvbijlemfv  45194  imasetpreimafvbijlemf1  45196  fargshiftfva  45235  ichreuopeq  45265  2exopprim  45317  reuopreuprim  45318  fmtnoprmfac1  45357  proththd  45406  opoeALTV  45475  evensumeven  45499  sbgoldbalt  45573  evengpop3  45590  evengpoap3  45591  nnsum4primeseven  45592  nnsum4primesevenALTV  45593  wtgoldbnnsum4prm  45594  bgoldbnnsum3prm  45596  tgoldbach  45609  isomushgr  45618  assintop  45743  isringrng  45779  rnglz  45782  c0snmgmhm  45812  zrrnghm  45815  uzlidlring  45827  2zrngnmrid  45848  cznrng  45853  rnghmsubcsetclem2  45874  rhmsubcsetclem2  45920  rhmsubcrngclem2  45926  lmodvsmdi  46058  lincsum  46110  lincsumcl  46112  el0ldep  46147  ldepspr  46154  lindssnlvec  46167  modn0mul  46206  m1modmmod  46207  nn0digval  46286  1arympt1fv  46325  eenglngeehlnmlem1  46423  rrx2linest  46428  line2  46438  itsclc0yqe  46447  r19.41dv  46487  setrec1lem3  46735  aacllem  46845