Theorem anim1ci 615

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 613	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 206  df-an 396

This theorem is referenced by:  elpwdifsn  4784  f1ocnv  6835  fcdmssb  7113  dfrecs3  8367  dfrecs3OLD  8368  odi  8574  snmapen  9033  infcntss  9316  lediv2a  12104  lbreu  12160  nn2ge  12235  dfceil2  13800  leexp1a  14136  faclbnd6  14255  ccatval3  14525  ccatalpha  14539  ccatswrd  14614  pfxccatin12lem2  14677  pfxccat3  14680  pfxccat3a  14684  repsdf2  14724  repswsymball  14725  relexpindlem  15006  dvdsdivcl  16255  nn0ehalf  16317  nn0oddm1d2  16324  nnoddm1d2  16325  sumeven  16326  ndvdssub  16348  coprmgcdb  16582  ncoprmgcdne1b  16583  divgcdcoprm0  16598  ncoprmlnprm  16662  vfermltl  16732  powm2modprm  16734  modprmn0modprm0  16738  dvdsprmpweqle  16817  prmgaplem4  16985  prmgaplem7  16988  cshwshashlem2  17028  efmndid  18802  efmndmnd  18803  gimcnv  19181  cygabl  19800  gsummptnn0fz  19895  rngimcnv  20347  lmimcnv  20904  ixpsnbasval  21053  rngqiprngghmlem1  21129  rngqiprngimf  21139  rng2idl1cntr  21147  rngringbdlem1  21148  fldidom  21206  matbas2  22244  scmatmats  22334  scmatscm  22336  scmatmulcl  22341  scmatf  22352  mdet1  22424  mdet0  22429  cramerimplem1  22506  cramer  22514  decpmatmul  22595  pmatcollpwscmat  22614  chfacfisf  22677  dv11cn  25855  logbgcd1irr  26641  cofcutr  27759  lnhl  28301  usgrfilem  29019  cplgr3v  29127  wlkreslem  29361  usgr2trlncl  29452  wwlksnextbi  29583  clwwlkccatlem  29677  clwwlkel  29734  clwwlknon1loop  29786  uhgr3cyclex  29870  eucrctshift  29931  1to3vfriswmgr  29968  frgrnbnb  29981  fusgreghash2wspv  30023  numclwwlk6  30078  frgrreggt1  30081  frgrregord013  30083  hhcmpl  30888  upgracycumgr  34599  bj-finsumval0  36622  indexa  37057  aks6d1c2p2  41416  rimcnv  41549  omord2i  42506  oeord2i  42515  oaun3lem1  42579  founiiun0  44340  or2expropbilem1  46193  fcoresfob  46233  fundmdfat  46288  reuopreuprim  46645  uspgrsprfo  46977  elbigolo1  47397  2sphere  47589  itsclquadb  47616  lubeldm2  47743  glbeldm2  47744