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  4753  f1ocnv  6812  fcdmssb  7094  dfrecs3  8341  odi  8543  snmapen  9009  infcntss  9273  lediv2a  12077  lbreu  12133  nn2ge  12213  dfceil2  13801  leexp1a  14140  faclbnd6  14264  ccatval3  14544  ccatalpha  14558  ccatswrd  14633  pfxccatin12lem2  14696  pfxccat3  14699  pfxccat3a  14703  repsdf2  14743  repswsymball  14744  relexpindlem  15029  dvdsdivcl  16286  nn0ehalf  16348  nn0oddm1d2  16355  nnoddm1d2  16356  sumeven  16357  ndvdssub  16379  coprmgcdb  16619  ncoprmgcdne1b  16620  divgcdcoprm0  16635  ncoprmlnprm  16698  vfermltl  16772  powm2modprm  16774  modprmn0modprm0  16778  dvdsprmpweqle  16857  prmgaplem4  17025  prmgaplem7  17028  cshwshashlem2  17067  efmndid  18815  efmndmnd  18816  gimcnv  19199  cygabl  19821  gsummptnn0fz  19916  rngimcnv  20365  fldidom  20680  lmimcnv  20974  ixpsnbasval  21115  rngqiprngghmlem1  21197  rngqiprngimf  21207  rng2idl1cntr  21215  rngringbdlem1  21216  matbas2  22308  scmatmats  22398  scmatscm  22400  scmatmulcl  22405  scmatf  22416  mdet1  22488  mdet0  22493  cramerimplem1  22570  cramer  22578  decpmatmul  22659  pmatcollpwscmat  22678  chfacfisf  22741  dv11cn  25906  logbgcd1irr  26704  cofcutr  27832  lnhl  28542  usgrfilem  29254  cplgr3v  29362  wlkreslem  29597  usgr2trlncl  29690  wwlksnextbi  29824  clwwlkccatlem  29918  clwwlkel  29975  clwwlknon1loop  30027  uhgr3cyclex  30111  eucrctshift  30172  1to3vfriswmgr  30209  frgrnbnb  30222  fusgreghash2wspv  30264  numclwwlk6  30319  frgrreggt1  30322  frgrregord013  30324  hhcmpl  31129  upgracycumgr  35140  bj-finsumval0  37273  indexa  37727  dmqsblocks  38845  aks6d1c2p2  42107  rimcnv  42505  omord2i  43290  oeord2i  43299  oaun3lem1  43363  founiiun0  45184  or2expropbilem1  47033  fcoresfob  47073  fundmdfat  47130  reuopreuprim  47527  grimedg  47935  grlictr  48007  clnbgr3stgrgrlic  48011  gpgedgvtx1  48053  gpg5nbgrvtx13starlem2  48063  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  uspgrsprfo  48136  elbigolo1  48546  2sphere  48738  itsclquadb  48765  lubeldm2  48944  glbeldm2  48945