Theorem anim1ci 624

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 622	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  elpwdifsn  4743  f1ocnv  6808  fcdmssb  7092  dfrecs3  8331  odi  8536  snmapen  9008  infcntss  9256  lediv2a  12076  lbreu  12132  nn2ge  12230  dfceil2  13839  leexp1a  14178  faclbnd6  14302  ccatval3  14582  ccatalpha  14597  ccatswrd  14672  pfxccatin12lem2  14734  pfxccat3  14737  pfxccat3a  14741  repsdf2  14781  repswsymball  14782  relexpindlem  15066  dvdsdivcl  16326  nn0ehalf  16388  nn0oddm1d2  16395  nnoddm1d2  16396  sumeven  16397  ndvdssub  16419  coprmgcdb  16659  ncoprmgcdne1b  16660  divgcdcoprm0  16675  ncoprmlnprm  16739  vfermltl  16813  powm2modprm  16815  modprmn0modprm0  16819  dvdsprmpweqle  16898  prmgaplem4  17066  prmgaplem7  17069  cshwshashlem2  17108  chnccat  18634  efmndid  18898  efmndmnd  18899  gimcnv  19283  cygabl  19907  gsummptnn0fz  20002  rngimcnv  20477  rimcnv  20506  fldidom  20793  lmimcnv  21107  ixpsnbasval  21248  rngqiprngghmlem1  21330  rngqiprngimf  21340  rng2idl1cntr  21348  rngringbdlem1  21349  matbas2  22454  scmatmats  22544  scmatscm  22546  scmatmulcl  22551  scmatf  22562  mdet1  22634  mdet0  22639  cramerimplem1  22716  cramer  22724  decpmatmul  22805  pmatcollpwscmat  22824  chfacfisf  22887  dv11cn  26036  logbgcd1irr  26829  cofcutr  27987  lnhl  28754  usgrfilem  29467  cplgr3v  29575  wlkreslem  29807  usgr2trlncl  29899  wwlksnextbi  30033  clwwlkccatlem  30130  clwwlkel  30187  clwwlknon1loop  30239  uhgr3cyclex  30323  eucrctshift  30384  1to3vfriswmgr  30421  frgrnbnb  30434  fusgreghash2wspv  30476  numclwwlk6  30531  frgrreggt1  30534  frgrregord013  30536  hhcmpl  31342  upgracycumgr  35451  bj-finsumval0  37725  indexa  38180  dmqsblocks  39414  aks6d1c2p2  42684  omord2i  43826  oeord2i  43835  oaun3lem1  43899  founiiun0  45716  or2expropbilem1  47574  fcoresfob  47614  fundmdfat  47671  reuopreuprim  48080  nprmmul1  48081  ppivalnnprm  48182  grimedg  48505  grlictr  48585  clnbgr3stgrgrlim  48589  clnbgr3stgrgrlic  48590  gpgedgvtx1  48632  gpg5nbgrvtx13starlem2  48642  pgnbgreunbgrlem3  48688  pgnbgreunbgrlem6  48694  uspgrsprfo  48718  elbigolo1  49127  2sphere  49319  itsclquadb  49346  lubeldm2  49525  glbeldm2  49526