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 398

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 209  df-an 399

This theorem is referenced by:  norassOLD  1530  elpwdifsn  4714  f1ocnv  6621  frnssb  6879  dfrecs3  8003  odi  8199  snmapen  8584  infcntss  8786  lediv2a  11528  lbreu  11585  nn2ge  11658  dfceil2  13203  leexp1a  13533  faclbnd6  13653  ccatval3  13927  ccatalpha  13941  ccatswrd  14024  pfxccatin12lem2  14087  pfxccat3  14090  pfxccat3a  14094  repsdf2  14134  repswsymball  14135  dvdsdivcl  15660  nn0ehalf  15723  nn0oddm1d2  15730  nnoddm1d2  15731  sumeven  15732  ndvdssub  15754  coprmgcdb  15987  ncoprmgcdne1b  15988  divgcdcoprm0  16003  ncoprmlnprm  16062  vfermltl  16132  powm2modprm  16134  modprmn0modprm0  16138  dvdsprmpweqle  16216  prmgaplem4  16384  prmgaplem7  16387  cshwshashlem2  16424  efmndid  18047  efmndmnd  18048  gimcnv  18401  cygabl  19004  gsummptnn0fz  19100  lmimcnv  19833  ixpsnbasval  19976  matbas2  21024  scmatmats  21114  scmatscm  21116  scmatmulcl  21121  scmatf  21132  mdet1  21204  mdet0  21209  cramerimplem1  21286  cramer  21294  decpmatmul  21374  pmatcollpwscmat  21393  chfacfisf  21456  dv11cn  24592  logbgcd1irr  25366  lnhl  26395  usgrfilem  27103  cplgr3v  27211  wlkreslem  27445  usgr2trlncl  27535  wwlksnextbi  27666  clwwlkccatlem  27761  clwwlkel  27819  clwwlknon1loop  27871  uhgr3cyclex  27955  eucrctshift  28016  1to3vfriswmgr  28053  frgrnbnb  28066  fusgreghash2wspv  28108  numclwwlk6  28163  frgrreggt1  28166  frgrregord013  28168  hhcmpl  28971  upgracycumgr  32395  bj-finsumval0  34561  indexa  35002  founiiun0  41444  or2expropbilem1  43261  fundmdfat  43322  reuopreuprim  43682  elbigolo1  44611  2sphere  44730  itsclquadb  44757