Theorem anim1ci 616

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 614	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  4739  f1ocnv  6771  fcdmssb  7050  dfrecs3  8287  odi  8489  snmapen  8955  infcntss  9202  lediv2a  12008  lbreu  12064  nn2ge  12144  dfceil2  13735  leexp1a  14074  faclbnd6  14198  ccatval3  14478  ccatalpha  14493  ccatswrd  14568  pfxccatin12lem2  14630  pfxccat3  14633  pfxccat3a  14637  repsdf2  14677  repswsymball  14678  relexpindlem  14962  dvdsdivcl  16219  nn0ehalf  16281  nn0oddm1d2  16288  nnoddm1d2  16289  sumeven  16290  ndvdssub  16312  coprmgcdb  16552  ncoprmgcdne1b  16553  divgcdcoprm0  16568  ncoprmlnprm  16631  vfermltl  16705  powm2modprm  16707  modprmn0modprm0  16711  dvdsprmpweqle  16790  prmgaplem4  16958  prmgaplem7  16961  cshwshashlem2  17000  chnccat  18524  efmndid  18788  efmndmnd  18789  gimcnv  19172  cygabl  19796  gsummptnn0fz  19891  rngimcnv  20367  fldidom  20679  lmimcnv  20994  ixpsnbasval  21135  rngqiprngghmlem1  21217  rngqiprngimf  21227  rng2idl1cntr  21235  rngringbdlem1  21236  matbas2  22329  scmatmats  22419  scmatscm  22421  scmatmulcl  22426  scmatf  22437  mdet1  22509  mdet0  22514  cramerimplem1  22591  cramer  22599  decpmatmul  22680  pmatcollpwscmat  22699  chfacfisf  22762  dv11cn  25926  logbgcd1irr  26724  cofcutr  27861  lnhl  28586  usgrfilem  29298  cplgr3v  29406  wlkreslem  29639  usgr2trlncl  29731  wwlksnextbi  29865  clwwlkccatlem  29959  clwwlkel  30016  clwwlknon1loop  30068  uhgr3cyclex  30152  eucrctshift  30213  1to3vfriswmgr  30250  frgrnbnb  30263  fusgreghash2wspv  30305  numclwwlk6  30360  frgrreggt1  30363  frgrregord013  30365  hhcmpl  31170  upgracycumgr  35165  bj-finsumval0  37298  indexa  37752  dmqsblocks  38870  aks6d1c2p2  42131  rimcnv  42529  omord2i  43313  oeord2i  43322  oaun3lem1  43386  founiiun0  45206  or2expropbilem1  47042  fcoresfob  47082  fundmdfat  47139  reuopreuprim  47536  grimedg  47945  grlictr  48025  clnbgr3stgrgrlim  48029  clnbgr3stgrgrlic  48030  gpgedgvtx1  48072  gpg5nbgrvtx13starlem2  48082  pgnbgreunbgrlem3  48128  pgnbgreunbgrlem6  48134  uspgrsprfo  48158  elbigolo1  48568  2sphere  48760  itsclquadb  48787  lubeldm2  48966  glbeldm2  48967