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  4747  f1ocnv  6794  fcdmssb  7076  dfrecs3  8314  odi  8516  snmapen  8987  infcntss  9235  lediv2a  12048  lbreu  12104  nn2ge  12184  dfceil2  13771  leexp1a  14110  faclbnd6  14234  ccatval3  14514  ccatalpha  14529  ccatswrd  14604  pfxccatin12lem2  14666  pfxccat3  14669  pfxccat3a  14673  repsdf2  14713  repswsymball  14714  relexpindlem  14998  dvdsdivcl  16255  nn0ehalf  16317  nn0oddm1d2  16324  nnoddm1d2  16325  sumeven  16326  ndvdssub  16348  coprmgcdb  16588  ncoprmgcdne1b  16589  divgcdcoprm0  16604  ncoprmlnprm  16667  vfermltl  16741  powm2modprm  16743  modprmn0modprm0  16747  dvdsprmpweqle  16826  prmgaplem4  16994  prmgaplem7  16997  cshwshashlem2  17036  chnccat  18561  efmndid  18825  efmndmnd  18826  gimcnv  19208  cygabl  19832  gsummptnn0fz  19927  rngimcnv  20404  fldidom  20716  lmimcnv  21031  ixpsnbasval  21172  rngqiprngghmlem1  21254  rngqiprngimf  21264  rng2idl1cntr  21272  rngringbdlem1  21273  matbas2  22377  scmatmats  22467  scmatscm  22469  scmatmulcl  22474  scmatf  22485  mdet1  22557  mdet0  22562  cramerimplem1  22639  cramer  22647  decpmatmul  22728  pmatcollpwscmat  22747  chfacfisf  22810  dv11cn  25974  logbgcd1irr  26772  cofcutr  27932  lnhl  28699  usgrfilem  29412  cplgr3v  29520  wlkreslem  29753  usgr2trlncl  29845  wwlksnextbi  29979  clwwlkccatlem  30076  clwwlkel  30133  clwwlknon1loop  30185  uhgr3cyclex  30269  eucrctshift  30330  1to3vfriswmgr  30367  frgrnbnb  30380  fusgreghash2wspv  30422  numclwwlk6  30477  frgrreggt1  30480  frgrregord013  30482  hhcmpl  31287  upgracycumgr  35366  bj-finsumval0  37529  indexa  37973  dmqsblocks  39207  aks6d1c2p2  42478  rimcnv  42876  omord2i  43647  oeord2i  43656  oaun3lem1  43720  founiiun0  45538  or2expropbilem1  47381  fcoresfob  47421  fundmdfat  47478  reuopreuprim  47875  grimedg  48284  grlictr  48364  clnbgr3stgrgrlim  48368  clnbgr3stgrgrlic  48369  gpgedgvtx1  48411  gpg5nbgrvtx13starlem2  48421  pgnbgreunbgrlem3  48467  pgnbgreunbgrlem6  48473  uspgrsprfo  48497  elbigolo1  48906  2sphere  49098  itsclquadb  49125  lubeldm2  49304  glbeldm2  49305