Theorem anim1ci 617

Description: Introduce conjunct to both sides of an implication. (Contributed by Peter Mazsa, 24-Sep-2022.)

Hypothesis

Ref	Expression
anim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
anim1ci	⊢ ((𝜑 ∧ 𝜒) → (𝜒 ∧ 𝜓))

Proof of Theorem anim1ci

Step	Hyp	Ref	Expression
1		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
2		id 22	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	anim12ci 615	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:  elpwdifsn  4735  f1ocnv  6794  fcdmssb  7076  dfrecs3  8314  odi  8516  snmapen  8987  infcntss  9235  lediv2a  12052  lbreu  12108  nn2ge  12206  dfceil2  13800  leexp1a  14139  faclbnd6  14263  ccatval3  14543  ccatalpha  14558  ccatswrd  14633  pfxccatin12lem2  14695  pfxccat3  14698  pfxccat3a  14702  repsdf2  14742  repswsymball  14743  relexpindlem  15027  dvdsdivcl  16287  nn0ehalf  16349  nn0oddm1d2  16356  nnoddm1d2  16357  sumeven  16358  ndvdssub  16380  coprmgcdb  16620  ncoprmgcdne1b  16621  divgcdcoprm0  16636  ncoprmlnprm  16700  vfermltl  16774  powm2modprm  16776  modprmn0modprm0  16780  dvdsprmpweqle  16859  prmgaplem4  17027  prmgaplem7  17030  cshwshashlem2  17069  chnccat  18594  efmndid  18858  efmndmnd  18859  gimcnv  19244  cygabl  19868  gsummptnn0fz  19963  rngimcnv  20438  fldidom  20750  lmimcnv  21064  ixpsnbasval  21205  rngqiprngghmlem1  21287  rngqiprngimf  21297  rng2idl1cntr  21305  rngringbdlem1  21306  matbas2  22388  scmatmats  22478  scmatscm  22480  scmatmulcl  22485  scmatf  22496  mdet1  22568  mdet0  22573  cramerimplem1  22650  cramer  22658  decpmatmul  22739  pmatcollpwscmat  22758  chfacfisf  22821  dv11cn  25970  logbgcd1irr  26760  cofcutr  27918  lnhl  28685  usgrfilem  29398  cplgr3v  29506  wlkreslem  29738  usgr2trlncl  29830  wwlksnextbi  29964  clwwlkccatlem  30061  clwwlkel  30118  clwwlknon1loop  30170  uhgr3cyclex  30254  eucrctshift  30315  1to3vfriswmgr  30352  frgrnbnb  30365  fusgreghash2wspv  30407  numclwwlk6  30462  frgrreggt1  30465  frgrregord013  30467  hhcmpl  31273  upgracycumgr  35337  bj-finsumval0  37601  indexa  38056  dmqsblocks  39290  aks6d1c2p2  42560  rimcnv  42964  omord2i  43731  oeord2i  43740  oaun3lem1  43804  founiiun0  45622  or2expropbilem1  47482  fcoresfob  47522  fundmdfat  47579  reuopreuprim  47988  nprmmul1  47989  ppivalnnprm  48090  grimedg  48413  grlictr  48493  clnbgr3stgrgrlim  48497  clnbgr3stgrgrlic  48498  gpgedgvtx1  48540  gpg5nbgrvtx13starlem2  48550  pgnbgreunbgrlem3  48596  pgnbgreunbgrlem6  48602  uspgrsprfo  48626  elbigolo1  49035  2sphere  49227  itsclquadb  49254  lubeldm2  49433  glbeldm2  49434