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 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 207  df-an 396

This theorem is referenced by:  sylanl1  680  sylanr1  682  eu6im  2575  r19.28v  3167  rmob  3840  eqeuel  4317  preq12nebg  4819  fores  6756  fdmeu  6890  ssimaex  6919  dffv2  6929  exfo  7050  fpropnf1  7213  f1ocoima  7249  oprabv  7418  ndmovass  7546  fun11uni  7875  resf1ext2b  7877  fabexgOLD  7881  f1oabexgOLD  7885  f1iun  7888  soxp  8071  tz7.48lem  8372  tz7.49c  8377  omass  8507  oewordri  8520  omabs  8579  sbthlem9  9023  pssnn  9093  fineqvlem  9166  domunfican  9222  fiint  9227  fsuppsssupp  9284  sup0  9370  inf1  9531  infeq5  9546  cantnfle  9580  rankuni  9775  djuunxp  9833  acndom  9961  acnnum  9962  cdainflem  10098  cfcof  10184  ac6num  10389  ac6s2  10396  brdom5  10439  brdom4  10440  genpnnp  10916  divmulasscom  11820  lediv2a  12036  supmul1  12111  infregelb  12126  nn2ge  12172  btwnz  12595  eluz2b2  12834  uz2mulcl  12839  eqreznegel  12847  xrsupexmnf  13220  xrinfmexpnf  13221  xrsupsslem  13222  xrinfmsslem  13223  supxrun  13231  ioo0  13286  elioo4g  13322  fz0fzelfz0  13550  fz0fzdiffz0  13553  2ffzeq  13565  elfzodifsumelfzo  13647  elfzom1elp1fzo  13648  zpnn0elfzo  13654  elfzom1elp1fzo1  13683  fzonfzoufzol  13687  quoremnn0  13776  zmodidfzoimp  13821  modabs  13824  modaddb  13829  modifeq2int  13856  modaddmulmod  13861  expcl2lem  13996  hashgt23el  14347  hashreshashfun  14362  iswrdsymb  14454  ccatcl  14497  ccatsymb  14506  swrdfv2  14585  swrdsbslen  14588  swrdspsleq  14589  pfxswrd  14629  pfxccatin12lem3  14655  pfxccatpfx2  14660  swrdccat3blem  14662  reuccatpfxs1  14670  repswccat  14709  cshweqdifid  14743  lswco  14762  repsco  14763  s4f1o  14841  trclun  14937  mulre  15044  rediv  15054  imdiv  15061  resqrex  15173  caurcvg2  15601  fsumdifsnconst  15714  modfsummods  15716  tanval  16053  p1modz1  16186  negdvdsb  16199  muldvds1  16207  muldvds2  16208  dvdscmulr  16211  dvdsmulcr  16212  sumodd  16315  divalglem8  16327  divgcdnn  16442  lcmfunsnlem2lem2  16566  lcmfun  16572  2mulprm  16620  maxprmfct  16636  vfermltlALT  16730  modprm0  16733  pcpremul  16771  pcmul  16779  oddprmdvds  16831  prmdvdsprmo  16970  cshwsidrepsw  17021  gsumccat  18766  grpissubg  19076  ecqusaddd  19121  ecqusaddcl  19122  eqg0subg  19125  gim0to0  19198  gsmsymgreqlem2  19360  symgfixfo  19368  fsfnn0gsumfsffz  19912  rnglz  20100  isringrng  20222  irredn0  20359  c0snmgmhm  20398  rimisrngim  20431  zrrnghm  20469  rnghmsubcsetclem2  20565  rhmsubcsetclem2  20594  rhmsubcrngclem2  20600  lsppratlem1  21102  qusmulrng  21237  quscrng  21238  rngqiprngghmlem3  21244  rngqiprnglinlem3  21248  rngqiprngimf1lem  21249  rngqiprnglin  21257  cnfldfunALT  21324  cnfldfunALTOLD  21337  dvdsrzring  21416  mpofrlmd  21732  matinvgcell  22379  mat1dimcrng  22421  dmatscmcl  22447  scmatscm  22457  scmatghm  22477  scmatmhm  22478  ma1repvcl  22514  slesolinv  22624  slesolinvbi  22625  cramerimplem1  22627  cramerimp  22630  cramerlem1  22631  cramer  22635  cpmatacl  22660  cpmatmcl  22663  mat2pmatghm  22674  mat2pmatmul  22675  m2pmfzgsumcl  22692  decpmatmul  22716  decpmatmulsumfsupp  22717  pmatcollpwfi  22726  pm2mpf1  22743  pm2mpghm  22760  pm2mpmhmlem1  22762  monmat2matmon  22768  chpdmatlem2  22783  chpdmat  22785  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  clscld  22991  neiptopnei  23076  2ndcdisj2  23401  comppfsc  23476  tx1stc  23594  opnfbas  23786  fbasfip  23812  alexsublem  23988  alexsubALTlem4  23994  cnextcn  24011  ngpocelbl  24648  cphipval  25199  bcthlem5  25284  vitalilem4  25568  vitalilem5  25569  itg2mulc  25704  bddiblnc  25799  dvcobr  25905  dvcobrOLD  25906  dvcnvlem  25936  dvferm1  25945  dvne0  25972  mdegmullem  26039  plyeq0lem  26171  plyexmo  26277  aalioulem5  26300  aalioulem6  26301  aaliou  26302  cxple2a  26664  cxpaddlelem  26717  cxpaddle  26718  relogbcxpb  26753  bcmono  27244  lgsprme0  27306  gausslemma2dlem0e  27327  gausslemma2dlem1a  27332  gausslemma2dlem6  27339  lgsquadlem2  27348  2lgsoddprm  27383  elno2  27622  cofcutr  27920  colinearalg  28983  axcontlem3  29039  umgrislfupgrlem  29195  edgupgr  29207  usgruspgrb  29256  usgrislfuspgr  29260  edgssv2  29271  umgr2edg  29282  uspgredg2v  29297  usgrexmplef  29332  subupgr  29360  subusgr  29362  nbupgrres  29437  nb3gr2nb  29457  nbupgruvtxres  29480  cusgrres  29522  cusgrsizeindslem  29525  cusgrsizeinds  29526  vtxdun  29555  finrusgrfusgr  29639  cusgrrusgr  29655  pthdifv  29803  spthdep  29807  cycliscrct  29872  crctcshwlkn0lem6  29888  crctcshwlkn0lem7  29889  crctcshtrl  29896  crctcsh  29897  umgr2adedgwlkonALT  30020  elwwlks2  30042  elwspths2spth  30043  rusgrnumwwlk  30051  clwlkclwwlklem2a  30073  clwlkclwwlklem3  30076  clwwisshclwws  30090  wwlksubclwwlk  30133  eleclclwwlknlem2  30136  eupth2lem3lem3  30305  eucrct2eupth1  30319  frgr3v  30350  3vfriswmgr  30353  1to3vfriswmgr  30355  3cyclfrgr  30363  vdgn1frgrv2  30371  frgrwopreglem5  30396  frgrwopreglem5ALT  30397  frrusgrord0lem  30414  frrusgrord0  30415  2clwwlk2clwwlk  30425  extwwlkfab  30427  numclwwlk1lem2fo  30433  friendshipgt3  30473  ex-natded9.20-2  30493  grpoidinvlem3  30581  grpoidinv  30583  nmobndseqi  30854  nmobndseqiALT  30855  hvaddsub4  31153  ocsh  31358  5oalem2  31730  5oalem5  31733  3oalem2  31738  pjjsi  31775  hoadddir  31879  leopmul  32209  stge1i  32313  hatomistici  32437  mdsymlem2  32479  mdsymlem5  32482  addltmulALT  32521  isoun  32781  fsumiunle  32910  lsmsnorb  33472  crefdf  34005  qqhre  34177  esumiun  34251  sxbrsigalem0  34428  dya2iocnei  34439  sxbrsigalem5  34445  sibfinima  34496  eulerpartlemgs2  34537  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemsup  34662  bnj529  34897  bnj945  34929  bnj1098  34939  bnj1533  35008  bnj605  35063  bnj594  35068  bnj607  35072  bnj966  35100  bnj967  35101  bnj996  35112  bnj999  35114  bnj1006  35116  bnj1118  35140  bnj1172  35157  bnj1279  35174  bnj1296  35177  bnj1498  35217  fnrelpredd  35247  lfuhgr3  35314  loop1cycl  35331  cvmsi  35459  satf0op  35571  satffunlem1lem1  35596  satffunlem2lem1  35598  fv2ndcnv  35972  trisegint  36222  funtransport  36225  btwnconn1lem4  36284  btwnconn2  36296  segcon2  36299  outsideofeu  36325  isfne  36533  lukshef-ax2  36609  limsucncmpi  36639  weiunso  36660  bj-nsnid  37271  bj-restn0b  37292  bj-eldiag2  37378  bj-isrvec2  37501  pibt2  37618  unccur  37800  lindsadd  37810  lindsenlbs  37812  matunitlindflem1  37813  matunitlindflem2  37814  poimirlem26  37843  poimirlem27  37844  poimirlem29  37846  poimirlem30  37847  poimirlem32  37849  heicant  37852  ismblfin  37858  itg2gt0cn  37872  areacirc  37910  opelopab3  37915  isdivrngo  38147  isdrngo2  38155  fldcrngo  38201  flddmn  38255  refrelredund4  38888  mainer2  39101  cmtbr4N  39511  linepsubN  40008  pmapsub  40024  paddasslem14  40089  pclcmpatN  40157  trlval2  40419  cdleme20  40580  cdleme21j  40592  dvalveclem  41281  dia2dimlem7  41326  dvhlveclem  41364  docaclN  41380  dihjat1  41685  mapdhcl  41983  mapdh6dN  41995  mapdh8  42044  hdmap1l6d  42069  hdmap10  42096  hdmaprnlem17N  42119  hdmaplkr  42169  hdmapip0  42171  hgmapvv  42182  aks6d1c4  42374  cmpfiiin  42935  pellexlem4  43070  pellqrex  43117  acongtr  43216  acongrep  43218  jm2.23  43234  omlimcl2  43480  onsucf1lem  43507  oege1  43544  nnoeomeqom  43550  cantnfresb  43562  onmcl  43569  tfsconcat0i  43583  ofoafg  43592  ofoafo  43594  ofoaass  43598  ofoacom  43599  naddcnfass  43607  rp-fakeanorass  43750  rp-isfinite6  43755  harval3  43775  inintabss  43815  rfovcnvf1od  44241  clsk1indlem3  44280  ntrclsk13  44308  pm10.55  44606  refsum2cnlem1  45278  axccd2  45470  mptssid  45481  fmuldfeq  45825  climsuse  45850  limclner  45891  climxlim2lem  46085  icccncfext  46127  stoweidlem26  46266  stoweidlem52  46292  stoweidlem57  46297  fourierdlem20  46367  fourierdlem41  46388  fourierdlem52  46398  fourierdlem64  46410  fourierdlem102  46448  fourierdlem114  46460  ovolval4lem1  46889  preimagelt  46939  preimalegt  46940  squeezedltsq  47128  funressneu  47289  afvelrn  47410  elfz2z  47557  2ffzoeq  47569  zplusmodne  47585  addmodne  47586  minusmod5ne  47591  modn0mul  47599  m1modmmod  47600  imasetpreimafvbijlemfv  47644  imasetpreimafvbijlemf1  47646  fargshiftfva  47685  ichreuopeq  47715  2exopprim  47767  reuopreuprim  47768  fmtnoprmfac1  47807  proththd  47856  opoeALTV  47925  evensumeven  47949  sbgoldbalt  48023  evengpop3  48040  evengpoap3  48041  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  wtgoldbnnsum4prm  48044  bgoldbnnsum3prm  48046  tgoldbach  48059  dfclnbgr6  48098  dfsclnbgr6  48100  uhgrimedg  48133  uhgrimprop  48134  isuspgrimlem  48137  isuspgrim  48138  gricushgr  48159  uhgrimisgrgric  48173  isubgr3stgrlem7  48214  uspgrlimlem2  48231  gpgedgel  48292  gpgprismgriedgdmss  48294  gpgedgvtx0  48303  gpgedgiov  48307  gpgedg2ov  48308  gpgedg2iv  48309  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem3  48315  gpg5nbgrvtx03star  48322  gpg5nbgr3star  48323  gpg5gricstgr3  48332  pgnbgreunbgrlem4  48361  assintop  48451  uzlidlring  48477  2zrngnmrid  48498  cznrng  48503  lmodvsmdi  48621  lincsum  48671  lincsumcl  48673  el0ldep  48708  ldepspr  48715  lindssnlvec  48728  nn0digval  48842  1arympt1fv  48881  eenglngeehlnmlem1  48979  rrx2linest  48984  line2  48994  itsclc0yqe  49003  r19.41dv  49043  setrec1lem3  49930  aacllem  50042