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 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 208  df-an 397

This theorem is referenced by:  sylanl1  676  sylanr1  678  eu6im  2618  r19.28v  3153  rmob  3802  eqeuel  4242  preq12nebg  4700  fores  6468  ssimaex  6615  dffv2  6623  exfo  6734  fpropnf1  6890  oprabv  7073  ndmovass  7192  fun11uni  7493  fabexg  7495  f1oabexg  7498  f1iun  7501  soxp  7676  tz7.48lem  7928  tz7.49c  7933  omass  8056  oewordri  8068  omabs  8124  sbthlem9  8482  fineqvlem  8578  pssnn  8582  domunfican  8637  fiint  8641  fsuppsssupp  8695  sup0  8776  inf1  8931  infeq5  8946  cantnfle  8980  rankuni  9138  djuunxp  9196  acndom  9323  acnnum  9324  cdainflem  9459  cfcof  9542  ac6num  9747  ac6s2  9754  brdom5  9797  brdom4  9798  genpnnp  10273  divmulasscom  11170  lediv2a  11382  supmul1  11458  infregelb  11473  nn2ge  11512  btwnz  11933  eluz2b2  12170  uz2mulcl  12175  eqreznegel  12183  xrsupexmnf  12548  xrinfmexpnf  12549  xrsupsslem  12550  xrinfmsslem  12551  supxrun  12559  ioo0  12613  elioo4g  12647  fz0fzelfz0  12863  fz0fzdiffz0  12866  2ffzeq  12878  elfzodifsumelfzo  12953  elfzom1elp1fzo  12954  zpnn0elfzo  12960  elfzom1elp1fzo1  12987  fzonfzoufzol  12990  quoremnn0  13074  zmodidfzoimp  13119  modabs  13122  modmuladd  13131  modifeq2int  13151  modaddmulmod  13156  expcl2lem  13291  hashgt23el  13633  hashreshashfun  13648  iswrdsymb  13727  ccatcl  13772  swrdfv2  13859  swrdsbslen  13862  swrdspsleq  13863  pfxswrd  13904  swrdccatin2  13927  pfxccatin12lem3  13930  pfxccatpfx2  13935  swrdccat3blem  13937  reuccatpfxs1  13945  repswccat  13984  2cshw  14011  cshweqdifid  14018  lswco  14037  repsco  14038  s4f1o  14116  ccat2s1fvwALT  14153  trclun  14208  mulre  14314  rediv  14324  imdiv  14331  resqrex  14444  caurcvg2  14868  fsumdifsnconst  14979  modfsummods  14981  tanval  15314  p1modz1  15447  negdvdsb  15459  muldvds1  15467  muldvds2  15468  dvdscmulr  15471  dvdsmulcr  15472  sumodd  15572  divalglem8  15584  divgcdnn  15696  lcmfunsnlem2lem2  15812  lcmfun  15818  2mulprm  15866  maxprmfct  15882  vfermltlALT  15968  modprm0  15971  pcpremul  16009  pcmul  16017  oddprmdvds  16068  prmdvdsprmo  16207  cshwsidrepsw  16256  gsmsymgreqlem2  18290  symgfixfo  18298  fsfnn0gsumfsffz  18820  irredn0  19143  gim0to0  19185  rim0to0OLD  19186  lsppratlem1  19609  dvdsrzring  20312  mpofrlmd  20603  matinvgcell  20728  mat1dimcrng  20770  dmatscmcl  20796  scmatscm  20806  scmatghm  20826  scmatmhm  20827  ma1repvcl  20863  slesolinv  20973  slesolinvbi  20974  cramerimplem1  20976  cramerimp  20979  cramerlem1  20980  cramer  20984  cpmatacl  21008  cpmatmcl  21011  mat2pmatghm  21022  mat2pmatmul  21023  m2pmfzgsumcl  21040  decpmatmul  21064  decpmatmulsumfsupp  21065  pmatcollpwfi  21074  pm2mpf1  21091  pm2mpghm  21108  pm2mpmhmlem1  21110  monmat2matmon  21116  chpdmatlem2  21131  chpdmat  21133  cpmadugsumlemB  21166  cpmadugsumlemC  21167  cpmadugsumlemF  21168  clscld  21339  neiptopnei  21424  2ndcdisj2  21749  comppfsc  21824  tx1stc  21942  opnfbas  22134  fbasfip  22160  alexsublem  22336  alexsubALTlem4  22342  cnextcn  22359  ngpocelbl  22996  cphipval  23529  bcthlem5  23614  vitalilem4  23895  vitalilem5  23896  itg2mulc  24031  dvcobr  24226  dvcnvlem  24256  dvferm1  24265  dvne0  24291  mdegmullem  24355  plyeq0lem  24483  plyexmo  24585  aalioulem5  24608  aalioulem6  24609  aaliou  24610  cxple2a  24963  cxpaddlelem  25013  cxpaddle  25014  relogbcxpb  25046  bcmono  25535  lgsprme0  25597  gausslemma2dlem0e  25618  gausslemma2dlem1a  25623  gausslemma2dlem6  25630  lgsquadlem2  25639  2lgsoddprm  25674  colinearalg  26379  axcontlem3  26435  umgrislfupgrlem  26590  edgupgr  26602  usgruspgrb  26649  usgrislfuspgr  26652  edgssv2  26663  umgr2edg  26674  uspgredg2v  26689  usgrexmplef  26724  subupgr  26752  subusgr  26754  nbupgrres  26829  nb3gr2nb  26849  nbupgruvtxres  26872  cusgrres  26913  cusgrsizeindslem  26916  cusgrsizeinds  26917  vtxdun  26946  finrusgrfusgr  27030  cusgrrusgr  27046  wlkreslemOLD  27136  spthdep  27202  cycliscrct  27267  crctcshwlkn0lem6  27280  crctcshwlkn0lem7  27281  crctcshtrl  27288  crctcsh  27289  umgr2adedgwlkonALT  27413  elwwlks2  27432  elwspths2spth  27433  rusgrnumwwlk  27441  clwlkclwwlklem2a  27463  clwlkclwwlklem3  27466  clwwisshclwws  27480  wwlksubclwwlk  27524  eleclclwwlknlem2  27527  eupth2lem3lem3  27697  eucrct2eupth1  27711  eucrct2eupth1OLD  27712  frgr3v  27746  3vfriswmgr  27749  1to3vfriswmgr  27751  3cyclfrgr  27759  vdgn1frgrv2  27767  frgrwopreglem5  27792  frgrwopreglem5ALT  27793  frrusgrord0lem  27810  frrusgrord0  27811  2clwwlk2clwwlk  27821  extwwlkfab  27823  numclwwlk1lem2fo  27829  friendshipgt3  27869  ex-natded9.20-2  27889  grpoidinvlem3  27974  grpoidinv  27976  nmobndseqi  28247  nmobndseqiALT  28248  hvaddsub4  28546  ocsh  28751  5oalem2  29123  5oalem5  29126  3oalem2  29131  pjjsi  29168  hoadddir  29272  leopmul  29602  stge1i  29706  hatomistici  29830  mdsymlem2  29872  mdsymlem5  29875  addltmulALT  29914  isoun  30125  fsumiunle  30229  crefdf  30729  qqhre  30878  esumiun  30970  sxbrsigalem0  31146  dya2iocnei  31157  sxbrsigalem5  31163  sibfinima  31214  eulerpartlemgs2  31255  ballotlemfc0  31367  ballotlemfcc  31368  ballotlemsup  31379  bnj529  31629  bnj945  31662  bnj1098  31672  bnj1533  31740  bnj605  31795  bnj594  31800  bnj607  31804  bnj966  31832  bnj967  31833  bnj996  31843  bnj999  31845  bnj1006  31847  bnj1118  31870  bnj1172  31887  bnj1279  31904  bnj1296  31907  bnj1498  31947  lfuhgr3  31978  loop1cycl  31992  cvmsi  32120  satf0op  32232  satffunlem1lem1  32257  satffunlem2lem1  32259  fv2ndcnv  32629  elno2  32770  trisegint  33098  funtransport  33101  btwnconn1lem4  33160  btwnconn2  33172  segcon2  33175  outsideofeu  33201  isfne  33296  lukshef-ax2  33372  limsucncmpi  33402  bj-nsnid  33960  bj-restn0b  33981  bj-elid3  34029  bj-eldiag2  34035  pibt2  34229  unccur  34406  lindsadd  34416  lindsenlbs  34418  matunitlindflem1  34419  matunitlindflem2  34420  poimirlem26  34449  poimirlem27  34450  poimirlem29  34452  poimirlem30  34453  poimirlem32  34455  heicant  34458  ismblfin  34464  itg2gt0cn  34478  bddiblnc  34493  areacirc  34518  opelopab3  34524  isdivrngo  34760  isdrngo2  34768  fldcrng  34814  flddmn  34868  refrelredund4  35401  cmtbr4N  35922  linepsubN  36419  pmapsub  36435  paddasslem14  36500  pclcmpatN  36568  trlval2  36830  cdleme20  36991  cdleme21j  37003  dvalveclem  37692  dia2dimlem7  37737  dvhlveclem  37775  docaclN  37791  dihjat1  38096  mapdhcl  38394  mapdh6dN  38406  mapdh8  38455  hdmap1l6d  38480  hdmap10  38507  hdmaprnlem17N  38530  hdmaplkr  38580  hdmapip0  38582  hgmapvv  38593  cmpfiiin  38779  pellexlem4  38914  pellqrex  38961  acongtr  39060  acongrep  39062  jm2.23  39078  rp-fakeanorass  39364  rp-isfinite6  39369  harval3  39389  inintabss  39423  rfovcnvf1od  39835  clsk1indlem3  39878  ntrclsk13  39906  pm10.55  40239  refsum2cnlem1  40833  axccd2  41036  mptssid  41052  fmuldfeq  41406  climsuse  41431  limclner  41474  climxlim2lem  41668  icccncfext  41711  stoweidlem26  41853  stoweidlem52  41879  stoweidlem57  41884  fourierdlem20  41954  fourierdlem41  41975  fourierdlem52  41985  fourierdlem64  41997  fourierdlem102  42035  fourierdlem114  42047  ovolval4lem1  42473  preimagelt  42522  preimalegt  42523  funressneu  42798  afvelrn  42883  elfz2z  43031  2ffzoeq  43044  fargshiftfva  43085  ichreuopeq  43117  2exopprim  43169  reuopreuprim  43170  fmtnoprmfac1  43209  proththd  43261  opoeALTV  43330  evensumeven  43354  sbgoldbalt  43428  evengpop3  43445  evengpoap3  43446  nnsum4primeseven  43447  nnsum4primesevenALTV  43448  wtgoldbnnsum4prm  43449  bgoldbnnsum3prm  43451  tgoldbach  43464  isomushgr  43473  uspgrsprfo  43505  assintop  43594  isringrng  43630  rnglz  43633  c0snmgmhm  43663  zrrnghm  43666  uzlidlring  43678  2zrngnmrid  43699  cznrng  43704  rnghmsubcsetclem2  43725  rhmsubcsetclem2  43771  rhmsubcrngclem2  43777  lmodvsmdi  43910  lincsum  43964  lincsumcl  43966  el0ldep  44001  ldepspr  44008  lindssnlvec  44021  modn0mul  44061  m1modmmod  44062  nn0digval  44141  eenglngeehlnmlem1  44205  rrx2linest  44210  line2  44220  itsclc0yqe  44229  setrec1lem3  44272  aacllem  44382