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  2569  r19.28v  3169  rmob  3856  eqeuel  4331  preq12nebg  4830  fores  6785  fdmeu  6920  ssimaex  6949  dffv2  6959  exfo  7080  fpropnf1  7245  f1ocoima  7281  oprabv  7452  ndmovass  7580  fun11uni  7912  resf1ext2b  7914  fabexgOLD  7918  f1oabexgOLD  7922  f1iun  7925  soxp  8111  tz7.48lem  8412  tz7.49c  8417  omass  8547  oewordri  8559  omabs  8618  sbthlem9  9065  pssnn  9138  fineqvlem  9216  domunfican  9279  fiint  9284  fiintOLD  9285  fsuppsssupp  9339  sup0  9425  inf1  9582  infeq5  9597  cantnfle  9631  rankuni  9823  djuunxp  9881  acndom  10011  acnnum  10012  cdainflem  10148  cfcof  10234  ac6num  10439  ac6s2  10446  brdom5  10489  brdom4  10490  genpnnp  10965  divmulasscom  11868  lediv2a  12084  supmul1  12159  infregelb  12174  nn2ge  12220  btwnz  12644  eluz2b2  12887  uz2mulcl  12892  eqreznegel  12900  xrsupexmnf  13272  xrinfmexpnf  13273  xrsupsslem  13274  xrinfmsslem  13275  supxrun  13283  ioo0  13338  elioo4g  13374  fz0fzelfz0  13602  fz0fzdiffz0  13605  2ffzeq  13617  elfzodifsumelfzo  13699  elfzom1elp1fzo  13700  zpnn0elfzo  13706  elfzom1elp1fzo1  13735  fzonfzoufzol  13738  quoremnn0  13825  zmodidfzoimp  13870  modabs  13873  modaddb  13878  modifeq2int  13905  modaddmulmod  13910  expcl2lem  14045  hashgt23el  14396  hashreshashfun  14411  iswrdsymb  14503  ccatcl  14546  ccatsymb  14554  swrdfv2  14633  swrdsbslen  14636  swrdspsleq  14637  pfxswrd  14678  pfxccatin12lem3  14704  pfxccatpfx2  14709  swrdccat3blem  14711  reuccatpfxs1  14719  repswccat  14758  cshweqdifid  14792  lswco  14812  repsco  14813  s4f1o  14891  trclun  14987  mulre  15094  rediv  15104  imdiv  15111  resqrex  15223  caurcvg2  15651  fsumdifsnconst  15764  modfsummods  15766  tanval  16103  p1modz1  16236  negdvdsb  16249  muldvds1  16257  muldvds2  16258  dvdscmulr  16261  dvdsmulcr  16262  sumodd  16365  divalglem8  16377  divgcdnn  16492  lcmfunsnlem2lem2  16616  lcmfun  16622  2mulprm  16670  maxprmfct  16686  vfermltlALT  16780  modprm0  16783  pcpremul  16821  pcmul  16829  oddprmdvds  16881  prmdvdsprmo  17020  cshwsidrepsw  17071  gsumccat  18775  grpissubg  19085  ecqusaddd  19131  ecqusaddcl  19132  eqg0subg  19135  gim0to0  19208  gsmsymgreqlem2  19368  symgfixfo  19376  fsfnn0gsumfsffz  19920  rnglz  20081  isringrng  20203  irredn0  20339  c0snmgmhm  20378  rimisrngim  20414  zrrnghm  20452  rnghmsubcsetclem2  20548  rhmsubcsetclem2  20577  rhmsubcrngclem2  20583  lsppratlem1  21064  qusmulrng  21199  quscrng  21200  rngqiprngghmlem3  21206  rngqiprnglinlem3  21210  rngqiprngimf1lem  21211  rngqiprnglin  21219  cnfldfunALT  21286  cnfldfunALTOLD  21299  dvdsrzring  21378  mpofrlmd  21693  matinvgcell  22329  mat1dimcrng  22371  dmatscmcl  22397  scmatscm  22407  scmatghm  22427  scmatmhm  22428  ma1repvcl  22464  slesolinv  22574  slesolinvbi  22575  cramerimplem1  22577  cramerimp  22580  cramerlem1  22581  cramer  22585  cpmatacl  22610  cpmatmcl  22613  mat2pmatghm  22624  mat2pmatmul  22625  m2pmfzgsumcl  22642  decpmatmul  22666  decpmatmulsumfsupp  22667  pmatcollpwfi  22676  pm2mpf1  22693  pm2mpghm  22710  pm2mpmhmlem1  22712  monmat2matmon  22718  chpdmatlem2  22733  chpdmat  22735  cpmadugsumlemB  22768  cpmadugsumlemC  22769  cpmadugsumlemF  22770  clscld  22941  neiptopnei  23026  2ndcdisj2  23351  comppfsc  23426  tx1stc  23544  opnfbas  23736  fbasfip  23762  alexsublem  23938  alexsubALTlem4  23944  cnextcn  23961  ngpocelbl  24599  cphipval  25150  bcthlem5  25235  vitalilem4  25519  vitalilem5  25520  itg2mulc  25655  bddiblnc  25750  dvcobr  25856  dvcobrOLD  25857  dvcnvlem  25887  dvferm1  25896  dvne0  25923  mdegmullem  25990  plyeq0lem  26122  plyexmo  26228  aalioulem5  26251  aalioulem6  26252  aaliou  26253  cxple2a  26615  cxpaddlelem  26668  cxpaddle  26669  relogbcxpb  26704  bcmono  27195  lgsprme0  27257  gausslemma2dlem0e  27278  gausslemma2dlem1a  27283  gausslemma2dlem6  27290  lgsquadlem2  27299  2lgsoddprm  27334  elno2  27573  cofcutr  27839  colinearalg  28844  axcontlem3  28900  umgrislfupgrlem  29056  edgupgr  29068  usgruspgrb  29117  usgrislfuspgr  29121  edgssv2  29132  umgr2edg  29143  uspgredg2v  29158  usgrexmplef  29193  subupgr  29221  subusgr  29223  nbupgrres  29298  nb3gr2nb  29318  nbupgruvtxres  29341  cusgrres  29383  cusgrsizeindslem  29386  cusgrsizeinds  29387  vtxdun  29416  finrusgrfusgr  29500  cusgrrusgr  29516  pthdifv  29667  spthdep  29671  cycliscrct  29736  crctcshwlkn0lem6  29752  crctcshwlkn0lem7  29753  crctcshtrl  29760  crctcsh  29761  umgr2adedgwlkonALT  29884  elwwlks2  29903  elwspths2spth  29904  rusgrnumwwlk  29912  clwlkclwwlklem2a  29934  clwlkclwwlklem3  29937  clwwisshclwws  29951  wwlksubclwwlk  29994  eleclclwwlknlem2  29997  eupth2lem3lem3  30166  eucrct2eupth1  30180  frgr3v  30211  3vfriswmgr  30214  1to3vfriswmgr  30216  3cyclfrgr  30224  vdgn1frgrv2  30232  frgrwopreglem5  30257  frgrwopreglem5ALT  30258  frrusgrord0lem  30275  frrusgrord0  30276  2clwwlk2clwwlk  30286  extwwlkfab  30288  numclwwlk1lem2fo  30294  friendshipgt3  30334  ex-natded9.20-2  30354  grpoidinvlem3  30442  grpoidinv  30444  nmobndseqi  30715  nmobndseqiALT  30716  hvaddsub4  31014  ocsh  31219  5oalem2  31591  5oalem5  31594  3oalem2  31599  pjjsi  31636  hoadddir  31740  leopmul  32070  stge1i  32174  hatomistici  32298  mdsymlem2  32340  mdsymlem5  32343  addltmulALT  32382  isoun  32632  fsumiunle  32761  lsmsnorb  33369  crefdf  33845  qqhre  34017  esumiun  34091  sxbrsigalem0  34269  dya2iocnei  34280  sxbrsigalem5  34286  sibfinima  34337  eulerpartlemgs2  34378  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemsup  34503  bnj529  34738  bnj945  34770  bnj1098  34780  bnj1533  34849  bnj605  34904  bnj594  34909  bnj607  34913  bnj966  34941  bnj967  34942  bnj996  34953  bnj999  34955  bnj1006  34957  bnj1118  34981  bnj1172  34998  bnj1279  35015  bnj1296  35018  bnj1498  35058  fnrelpredd  35086  lfuhgr3  35114  loop1cycl  35131  cvmsi  35259  satf0op  35371  satffunlem1lem1  35396  satffunlem2lem1  35398  fv2ndcnv  35772  trisegint  36023  funtransport  36026  btwnconn1lem4  36085  btwnconn2  36097  segcon2  36100  outsideofeu  36126  isfne  36334  lukshef-ax2  36410  limsucncmpi  36440  weiunso  36461  bj-nsnid  37065  bj-restn0b  37086  bj-eldiag2  37172  bj-isrvec2  37295  pibt2  37412  unccur  37604  lindsadd  37614  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  poimirlem30  37651  poimirlem32  37653  heicant  37656  ismblfin  37662  itg2gt0cn  37676  areacirc  37714  opelopab3  37719  isdivrngo  37951  isdrngo2  37959  fldcrngo  38005  flddmn  38059  refrelredund4  38633  mainer2  38845  cmtbr4N  39255  linepsubN  39753  pmapsub  39769  paddasslem14  39834  pclcmpatN  39902  trlval2  40164  cdleme20  40325  cdleme21j  40337  dvalveclem  41026  dia2dimlem7  41071  dvhlveclem  41109  docaclN  41125  dihjat1  41430  mapdhcl  41728  mapdh6dN  41740  mapdh8  41789  hdmap1l6d  41814  hdmap10  41841  hdmaprnlem17N  41864  hdmaplkr  41914  hdmapip0  41916  hgmapvv  41927  aks6d1c4  42119  cmpfiiin  42692  pellexlem4  42827  pellqrex  42874  acongtr  42974  acongrep  42976  jm2.23  42992  omlimcl2  43238  onsucf1lem  43265  oege1  43302  nnoeomeqom  43308  cantnfresb  43320  onmcl  43327  tfsconcat0i  43341  ofoafg  43350  ofoafo  43352  ofoaass  43356  ofoacom  43357  naddcnfass  43365  rp-fakeanorass  43509  rp-isfinite6  43514  harval3  43534  inintabss  43574  rfovcnvf1od  44000  clsk1indlem3  44039  ntrclsk13  44067  pm10.55  44365  refsum2cnlem1  45038  axccd2  45231  mptssid  45242  fmuldfeq  45588  climsuse  45613  limclner  45656  climxlim2lem  45850  icccncfext  45892  stoweidlem26  46031  stoweidlem52  46057  stoweidlem57  46062  fourierdlem20  46132  fourierdlem41  46153  fourierdlem52  46163  fourierdlem64  46175  fourierdlem102  46213  fourierdlem114  46225  ovolval4lem1  46654  preimagelt  46704  preimalegt  46705  squeezedltsq  46894  funressneu  47052  afvelrn  47173  elfz2z  47320  2ffzoeq  47332  zplusmodne  47348  addmodne  47349  minusmod5ne  47354  modn0mul  47362  m1modmmod  47363  imasetpreimafvbijlemfv  47407  imasetpreimafvbijlemf1  47409  fargshiftfva  47448  ichreuopeq  47478  2exopprim  47530  reuopreuprim  47531  fmtnoprmfac1  47570  proththd  47619  opoeALTV  47688  evensumeven  47712  sbgoldbalt  47786  evengpop3  47803  evengpoap3  47804  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  tgoldbach  47822  dfclnbgr6  47860  dfsclnbgr6  47862  uhgrimedg  47895  uhgrimprop  47896  isuspgrimlem  47899  isuspgrim  47900  gricushgr  47921  uhgrimisgrgric  47935  isubgr3stgrlem7  47975  uspgrlimlem2  47992  gpgedgel  48045  gpgprismgriedgdmss  48047  gpgedgvtx0  48056  gpgedgiov  48060  gpgedg2ov  48061  gpgedg2iv  48062  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem3  48068  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  gpg5gricstgr3  48085  pgnbgreunbgrlem4  48113  assintop  48201  uzlidlring  48227  2zrngnmrid  48248  cznrng  48253  lmodvsmdi  48371  lincsum  48422  lincsumcl  48424  el0ldep  48459  ldepspr  48466  lindssnlvec  48479  nn0digval  48593  1arympt1fv  48632  eenglngeehlnmlem1  48730  rrx2linest  48735  line2  48745  itsclc0yqe  48754  r19.41dv  48794  setrec1lem3  49682  aacllem  49794