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  37296  bj-eldiag2  37382  bj-isrvec2  37505  pibt2  37622  unccur  37804  lindsadd  37814  lindsenlbs  37816  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem26  37847  poimirlem27  37848  poimirlem29  37850  poimirlem30  37851  poimirlem32  37853  heicant  37856  ismblfin  37862  itg2gt0cn  37876  areacirc  37914  opelopab3  37919  isdivrngo  38151  isdrngo2  38159  fldcrngo  38205  flddmn  38259  refrelredund4  38892  mainer2  39105  cmtbr4N  39515  linepsubN  40012  pmapsub  40028  paddasslem14  40093  pclcmpatN  40161  trlval2  40423  cdleme20  40584  cdleme21j  40596  dvalveclem  41285  dia2dimlem7  41330  dvhlveclem  41368  docaclN  41384  dihjat1  41689  mapdhcl  41987  mapdh6dN  41999  mapdh8  42048  hdmap1l6d  42073  hdmap10  42100  hdmaprnlem17N  42123  hdmaplkr  42173  hdmapip0  42175  hgmapvv  42186  aks6d1c4  42378  cmpfiiin  42939  pellexlem4  43074  pellqrex  43121  acongtr  43220  acongrep  43222  jm2.23  43238  omlimcl2  43484  onsucf1lem  43511  oege1  43548  nnoeomeqom  43554  cantnfresb  43566  onmcl  43573  tfsconcat0i  43587  ofoafg  43596  ofoafo  43598  ofoaass  43602  ofoacom  43603  naddcnfass  43611  rp-fakeanorass  43754  rp-isfinite6  43759  harval3  43779  inintabss  43819  rfovcnvf1od  44245  clsk1indlem3  44284  ntrclsk13  44312  pm10.55  44610  refsum2cnlem1  45282  axccd2  45474  mptssid  45485  fmuldfeq  45829  climsuse  45854  limclner  45895  climxlim2lem  46089  icccncfext  46131  stoweidlem26  46270  stoweidlem52  46296  stoweidlem57  46301  fourierdlem20  46371  fourierdlem41  46392  fourierdlem52  46402  fourierdlem64  46414  fourierdlem102  46452  fourierdlem114  46464  ovolval4lem1  46893  preimagelt  46943  preimalegt  46944  squeezedltsq  47132  funressneu  47293  afvelrn  47414  elfz2z  47561  2ffzoeq  47573  zplusmodne  47589  addmodne  47590  minusmod5ne  47595  modn0mul  47603  m1modmmod  47604  imasetpreimafvbijlemfv  47648  imasetpreimafvbijlemf1  47650  fargshiftfva  47689  ichreuopeq  47719  2exopprim  47771  reuopreuprim  47772  fmtnoprmfac1  47811  proththd  47860  opoeALTV  47929  evensumeven  47953  sbgoldbalt  48027  evengpop3  48044  evengpoap3  48045  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  tgoldbach  48063  dfclnbgr6  48102  dfsclnbgr6  48104  uhgrimedg  48137  uhgrimprop  48138  isuspgrimlem  48141  isuspgrim  48142  gricushgr  48163  uhgrimisgrgric  48177  isubgr3stgrlem7  48218  uspgrlimlem2  48235  gpgedgel  48296  gpgprismgriedgdmss  48298  gpgedgvtx0  48307  gpgedgiov  48311  gpgedg2ov  48312  gpgedg2iv  48313  gpg5nbgrvtx03starlem2  48315  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem3  48319  gpg5nbgrvtx03star  48326  gpg5nbgr3star  48327  gpg5gricstgr3  48336  pgnbgreunbgrlem4  48365  assintop  48455  uzlidlring  48481  2zrngnmrid  48502  cznrng  48507  lmodvsmdi  48625  lincsum  48675  lincsumcl  48677  el0ldep  48712  ldepspr  48719  lindssnlvec  48732  nn0digval  48846  1arympt1fv  48885  eenglngeehlnmlem1  48983  rrx2linest  48988  line2  48998  itsclc0yqe  49007  r19.41dv  49047  setrec1lem3  49934  aacllem  50046