Theorem anim1ci 622

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  elpwdifsn  4729  f1ocnv  6786  fcdmssb  7070  dfrecs3  8309  odi  8511  snmapen  8982  infcntss  9230  lediv2a  12048  lbreu  12104  nn2ge  12202  dfceil2  13796  leexp1a  14135  faclbnd6  14259  ccatval3  14539  ccatalpha  14554  ccatswrd  14629  pfxccatin12lem2  14691  pfxccat3  14694  pfxccat3a  14698  repsdf2  14738  repswsymball  14739  relexpindlem  15023  dvdsdivcl  16283  nn0ehalf  16345  nn0oddm1d2  16352  nnoddm1d2  16353  sumeven  16354  ndvdssub  16376  coprmgcdb  16616  ncoprmgcdne1b  16617  divgcdcoprm0  16632  ncoprmlnprm  16696  vfermltl  16770  powm2modprm  16772  modprmn0modprm0  16776  dvdsprmpweqle  16855  prmgaplem4  17023  prmgaplem7  17026  cshwshashlem2  17065  chnccat  18590  efmndid  18854  efmndmnd  18855  gimcnv  19240  cygabl  19864  gsummptnn0fz  19959  rngimcnv  20434  rimcnv  20463  fldidom  20750  lmimcnv  21064  ixpsnbasval  21205  rngqiprngghmlem1  21287  rngqiprngimf  21297  rng2idl1cntr  21305  rngringbdlem1  21306  matbas2  22411  scmatmats  22501  scmatscm  22503  scmatmulcl  22508  scmatf  22519  mdet1  22591  mdet0  22596  cramerimplem1  22673  cramer  22681  decpmatmul  22762  pmatcollpwscmat  22781  chfacfisf  22844  dv11cn  25993  logbgcd1irr  26783  cofcutr  27941  lnhl  28708  usgrfilem  29421  cplgr3v  29529  wlkreslem  29761  usgr2trlncl  29853  wwlksnextbi  29987  clwwlkccatlem  30084  clwwlkel  30141  clwwlknon1loop  30193  uhgr3cyclex  30277  eucrctshift  30338  1to3vfriswmgr  30375  frgrnbnb  30388  fusgreghash2wspv  30430  numclwwlk6  30485  frgrreggt1  30488  frgrregord013  30490  hhcmpl  31296  upgracycumgr  35382  bj-finsumval0  37646  indexa  38101  dmqsblocks  39335  aks6d1c2p2  42605  omord2i  43747  oeord2i  43756  oaun3lem1  43820  founiiun0  45638  or2expropbilem1  47496  fcoresfob  47536  fundmdfat  47593  reuopreuprim  48002  nprmmul1  48003  ppivalnnprm  48104  grimedg  48427  grlictr  48507  clnbgr3stgrgrlim  48511  clnbgr3stgrgrlic  48512  gpgedgvtx1  48554  gpg5nbgrvtx13starlem2  48564  pgnbgreunbgrlem3  48610  pgnbgreunbgrlem6  48616  uspgrsprfo  48640  elbigolo1  49049  2sphere  49241  itsclquadb  49268  lubeldm2  49447  glbeldm2  49448