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

This theorem is referenced by:  norassOLD  1536  elpwdifsn  4722  f1ocnv  6728  frnssb  6995  dfrecs3  8203  dfrecs3OLD  8204  odi  8410  snmapen  8828  infcntss  9088  lediv2a  11869  lbreu  11925  nn2ge  12000  dfceil2  13559  leexp1a  13893  faclbnd6  14013  ccatval3  14284  ccatalpha  14298  ccatswrd  14381  pfxccatin12lem2  14444  pfxccat3  14447  pfxccat3a  14451  repsdf2  14491  repswsymball  14492  relexpindlem  14774  dvdsdivcl  16025  nn0ehalf  16087  nn0oddm1d2  16094  nnoddm1d2  16095  sumeven  16096  ndvdssub  16118  coprmgcdb  16354  ncoprmgcdne1b  16355  divgcdcoprm0  16370  ncoprmlnprm  16432  vfermltl  16502  powm2modprm  16504  modprmn0modprm0  16508  dvdsprmpweqle  16587  prmgaplem4  16755  prmgaplem7  16758  cshwshashlem2  16798  efmndid  18527  efmndmnd  18528  gimcnv  18883  cygabl  19491  gsummptnn0fz  19587  lmimcnv  20329  ixpsnbasval  20480  fldidom  20576  matbas2  21570  scmatmats  21660  scmatscm  21662  scmatmulcl  21667  scmatf  21678  mdet1  21750  mdet0  21755  cramerimplem1  21832  cramer  21840  decpmatmul  21921  pmatcollpwscmat  21940  chfacfisf  22003  dv11cn  25165  logbgcd1irr  25944  lnhl  26976  usgrfilem  27694  cplgr3v  27802  wlkreslem  28037  usgr2trlncl  28128  wwlksnextbi  28259  clwwlkccatlem  28353  clwwlkel  28410  clwwlknon1loop  28462  uhgr3cyclex  28546  eucrctshift  28607  1to3vfriswmgr  28644  frgrnbnb  28657  fusgreghash2wspv  28699  numclwwlk6  28754  frgrreggt1  28757  frgrregord013  28759  hhcmpl  29562  upgracycumgr  33115  cofcutr  34092  bj-finsumval0  35456  indexa  35891  founiiun0  42728  or2expropbilem1  44526  fcoresfob  44566  fundmdfat  44621  reuopreuprim  44978  uspgrsprfo  45310  elbigolo1  45903  2sphere  46095  itsclquadb  46122  lubeldm2  46250  glbeldm2  46251