Theorem anim1ci 618

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  norassOLD  1535  elpwdifsn  4682  f1ocnv  6602  frnssb  6862  dfrecs3  7992  odi  8188  snmapen  8573  infcntss  8776  lediv2a  11523  lbreu  11578  nn2ge  11652  dfceil2  13204  leexp1a  13535  faclbnd6  13655  ccatval3  13924  ccatalpha  13938  ccatswrd  14021  pfxccatin12lem2  14084  pfxccat3  14087  pfxccat3a  14091  repsdf2  14131  repswsymball  14132  relexpindlem  14414  dvdsdivcl  15658  nn0ehalf  15719  nn0oddm1d2  15726  nnoddm1d2  15727  sumeven  15728  ndvdssub  15750  coprmgcdb  15983  ncoprmgcdne1b  15984  divgcdcoprm0  15999  ncoprmlnprm  16058  vfermltl  16128  powm2modprm  16130  modprmn0modprm0  16134  dvdsprmpweqle  16212  prmgaplem4  16380  prmgaplem7  16383  cshwshashlem2  16422  efmndid  18045  efmndmnd  18046  gimcnv  18399  cygabl  19003  gsummptnn0fz  19099  lmimcnv  19832  ixpsnbasval  19975  matbas2  21026  scmatmats  21116  scmatscm  21118  scmatmulcl  21123  scmatf  21134  mdet1  21206  mdet0  21211  cramerimplem1  21288  cramer  21296  decpmatmul  21377  pmatcollpwscmat  21396  chfacfisf  21459  dv11cn  24604  logbgcd1irr  25380  lnhl  26409  usgrfilem  27117  cplgr3v  27225  wlkreslem  27459  usgr2trlncl  27549  wwlksnextbi  27680  clwwlkccatlem  27774  clwwlkel  27831  clwwlknon1loop  27883  uhgr3cyclex  27967  eucrctshift  28028  1to3vfriswmgr  28065  frgrnbnb  28078  fusgreghash2wspv  28120  numclwwlk6  28175  frgrreggt1  28178  frgrregord013  28180  hhcmpl  28983  upgracycumgr  32513  bj-finsumval0  34700  indexa  35171  founiiun0  41817  or2expropbilem1  43624  fundmdfat  43685  reuopreuprim  44043  elbigolo1  44971  2sphere  45163  itsclquadb  45190