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  4733  f1ocnv  6784  fcdmssb  7066  dfrecs3  8303  odi  8505  snmapen  8976  infcntss  9224  lediv2a  12039  lbreu  12095  nn2ge  12193  dfceil2  13787  leexp1a  14126  faclbnd6  14250  ccatval3  14530  ccatalpha  14545  ccatswrd  14620  pfxccatin12lem2  14682  pfxccat3  14685  pfxccat3a  14689  repsdf2  14729  repswsymball  14730  relexpindlem  15014  dvdsdivcl  16274  nn0ehalf  16336  nn0oddm1d2  16343  nnoddm1d2  16344  sumeven  16345  ndvdssub  16367  coprmgcdb  16607  ncoprmgcdne1b  16608  divgcdcoprm0  16623  ncoprmlnprm  16687  vfermltl  16761  powm2modprm  16763  modprmn0modprm0  16767  dvdsprmpweqle  16846  prmgaplem4  17014  prmgaplem7  17017  cshwshashlem2  17056  chnccat  18581  efmndid  18845  efmndmnd  18846  gimcnv  19231  cygabl  19855  gsummptnn0fz  19950  rngimcnv  20425  fldidom  20737  lmimcnv  21052  ixpsnbasval  21193  rngqiprngghmlem1  21275  rngqiprngimf  21285  rng2idl1cntr  21293  rngringbdlem1  21294  matbas2  22395  scmatmats  22485  scmatscm  22487  scmatmulcl  22492  scmatf  22503  mdet1  22575  mdet0  22580  cramerimplem1  22657  cramer  22665  decpmatmul  22746  pmatcollpwscmat  22765  chfacfisf  22828  dv11cn  25978  logbgcd1irr  26775  cofcutr  27935  lnhl  28702  usgrfilem  29415  cplgr3v  29523  wlkreslem  29756  usgr2trlncl  29848  wwlksnextbi  29982  clwwlkccatlem  30079  clwwlkel  30136  clwwlknon1loop  30188  uhgr3cyclex  30272  eucrctshift  30333  1to3vfriswmgr  30370  frgrnbnb  30383  fusgreghash2wspv  30425  numclwwlk6  30480  frgrreggt1  30483  frgrregord013  30485  hhcmpl  31291  upgracycumgr  35356  bj-finsumval0  37612  indexa  38065  dmqsblocks  39299  aks6d1c2p2  42569  rimcnv  42973  omord2i  43744  oeord2i  43753  oaun3lem1  43817  founiiun0  45635  or2expropbilem1  47477  fcoresfob  47517  fundmdfat  47574  reuopreuprim  47983  nprmmul1  47984  ppivalnnprm  48085  grimedg  48408  grlictr  48488  clnbgr3stgrgrlim  48492  clnbgr3stgrgrlic  48493  gpgedgvtx1  48535  gpg5nbgrvtx13starlem2  48545  pgnbgreunbgrlem3  48591  pgnbgreunbgrlem6  48597  uspgrsprfo  48621  elbigolo1  49030  2sphere  49222  itsclquadb  49249  lubeldm2  49428  glbeldm2  49429