Theorem anim1ci 628

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 23	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	anim12ci 626	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜒 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  elpwdifsn  4751  f1ocnv  6825  fcdmssb  7110  dfrecs3  8358  odi  8565  snmapen  9044  infcntss  9292  lediv2a  12181  lbreu  12237  nn2ge  12335  dfceil2  13948  leexp1a  14287  faclbnd6  14411  ccatval3  14692  ccatalpha  14708  ccatswrd  14786  pfxccatin12lem2  14848  pfxccat3  14851  pfxccat3a  14855  repsdf2  14897  repswsymball  14898  relexpindlem  15184  dvdsdivcl  16454  nn0ehalf  16516  nn0oddm1d2  16523  nnoddm1d2  16524  sumeven  16525  ndvdssub  16547  coprmgcdb  16787  ncoprmgcdne1b  16788  divgcdcoprm0  16803  ncoprmlnprm  16867  vfermltl  16941  powm2modprm  16943  modprmn0modprm0  16947  dvdsprmpweqle  17026  prmgaplem4  17194  prmgaplem7  17197  cshwshashlem2  17236  chnccat  18762  mgmn0plusgf  18789  efmndid  19046  efmndmnd  19047  gimcnv  19443  cygabl  20067  gsummptnn0fz  20162  rngimcnv  20648  rimcnv  20679  fldidom  20991  lmimcnv  21304  ixpsnbasval  21445  rngqiprngghmlem1  21545  rngqiprngimf  21555  rng2idl1cntr  21563  rngringbdlem1  21564  matbas2  22698  scmatmats  22788  scmatscm  22790  scmatmulcl  22795  scmatf  22806  mdet1  22878  mdet0  22883  cramerimplem1  22963  cramer  22971  decpmatmul  23052  pmatcollpwscmat  23071  chfacfisf  23134  dv11cn  26283  logbgcd1irr  27086  cofcutr  28244  lnhl  29015  elplng  29192  usgrfilem  29842  cplgr3v  29950  wlkreslem  30182  usgr2trlncl  30280  wwlksnextbi  30417  clwwlkccatlem  30514  clwwlkel  30571  clwwlknon1loop  30623  uhgr3cyclex  30717  eucrctshift  30778  1to3vfriswmgr  30815  frgrnbnb  30828  fusgreghash2wspv  30870  numclwwlk6  30925  frgrreggt1  30928  frgrregord013  30930  hhcmpl  31736  upgracycumgr  35839  bj-finsumval0  38126  indexa  38587  dmqsblocks  39819  aks6d1c2p2  43089  omord2i  44246  oeord2i  44255  oaun3lem1  44319  founiiun0  46126  or2expropbilem1  48024  fcoresfob  48064  fundmdfat  48121  reuopreuprim  48530  nprmmul1  48531  ppivalnnprm  48632  grimedg  48955  grlictr  49035  clnbgr3stgrgrlim  49039  clnbgr3stgrgrlic  49040  gpgedgvtx1  49082  gpg5nbgrvtx13starlem2  49092  pgnbgreunbgrlem3  49138  pgnbgreunbgrlem6  49144  uspgrsprfo  49168  elbigolo1  49591  2sphere  49783  itsclquadb  49810  lubeldm2  49986  glbeldm2  49987