Theorem anim1ci 627

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  elpwdifsn  4756  f1ocnv  6833  fcdmssb  7117  dfrecs3  8358  odi  8563  snmapen  9034  infcntss  9281  lediv2a  12108  lbreu  12164  nn2ge  12262  dfceil2  13872  leexp1a  14211  faclbnd6  14335  ccatval3  14616  ccatalpha  14631  ccatswrd  14706  pfxccatin12lem2  14768  pfxccat3  14771  pfxccat3a  14775  repsdf2  14815  repswsymball  14816  relexpindlem  15100  dvdsdivcl  16373  nn0ehalf  16435  nn0oddm1d2  16442  nnoddm1d2  16443  sumeven  16444  ndvdssub  16466  coprmgcdb  16706  ncoprmgcdne1b  16707  divgcdcoprm0  16722  ncoprmlnprm  16786  vfermltl  16860  powm2modprm  16862  modprmn0modprm0  16866  dvdsprmpweqle  16945  prmgaplem4  17113  prmgaplem7  17116  cshwshashlem2  17155  chnccat  18681  efmndid  18946  efmndmnd  18947  gimcnv  19336  cygabl  19960  gsummptnn0fz  20055  rngimcnv  20537  rimcnv  20566  fldidom  20854  lmimcnv  21167  ixpsnbasval  21308  rngqiprngghmlem1  21406  rngqiprngimf  21416  rng2idl1cntr  21424  rngringbdlem1  21425  matbas2  22557  scmatmats  22647  scmatscm  22649  scmatmulcl  22654  scmatf  22665  mdet1  22737  mdet0  22742  cramerimplem1  22819  cramer  22827  decpmatmul  22908  pmatcollpwscmat  22927  chfacfisf  22990  dv11cn  26139  logbgcd1irr  26935  cofcutr  28093  lnhl  28863  elplng  29036  usgrfilem  29643  cplgr3v  29751  wlkreslem  29983  usgr2trlncl  30075  wwlksnextbi  30209  clwwlkccatlem  30306  clwwlkel  30363  clwwlknon1loop  30415  uhgr3cyclex  30499  eucrctshift  30560  1to3vfriswmgr  30597  frgrnbnb  30610  fusgreghash2wspv  30652  numclwwlk6  30707  frgrreggt1  30710  frgrregord013  30712  hhcmpl  31518  upgracycumgr  35611  bj-finsumval0  37895  indexa  38350  dmqsblocks  39584  aks6d1c2p2  42854  omord2i  43998  oeord2i  44007  oaun3lem1  44071  founiiun0  45878  or2expropbilem1  47736  fcoresfob  47776  fundmdfat  47833  reuopreuprim  48242  nprmmul1  48243  ppivalnnprm  48344  grimedg  48667  grlictr  48747  clnbgr3stgrgrlim  48751  clnbgr3stgrgrlic  48752  gpgedgvtx1  48794  gpg5nbgrvtx13starlem2  48804  pgnbgreunbgrlem3  48850  pgnbgreunbgrlem6  48856  uspgrsprfo  48880  elbigolo1  49304  2sphere  49496  itsclquadb  49523  lubeldm2  49701  glbeldm2  49702