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  1534  elpwdifsn  4721  f1ocnv  6627  frnssb  6885  dfrecs3  8009  odi  8205  snmapen  8590  infcntss  8792  lediv2a  11534  lbreu  11591  nn2ge  11665  dfceil2  13210  leexp1a  13540  faclbnd6  13660  ccatval3  13933  ccatalpha  13947  ccatswrd  14030  pfxccatin12lem2  14093  pfxccat3  14096  pfxccat3a  14100  repsdf2  14140  repswsymball  14141  dvdsdivcl  15666  nn0ehalf  15729  nn0oddm1d2  15736  nnoddm1d2  15737  sumeven  15738  ndvdssub  15760  coprmgcdb  15993  ncoprmgcdne1b  15994  divgcdcoprm0  16009  ncoprmlnprm  16068  vfermltl  16138  powm2modprm  16140  modprmn0modprm0  16144  dvdsprmpweqle  16222  prmgaplem4  16390  prmgaplem7  16393  cshwshashlem2  16430  efmndid  18053  efmndmnd  18054  gimcnv  18407  cygabl  19010  gsummptnn0fz  19106  lmimcnv  19839  ixpsnbasval  19982  matbas2  21030  scmatmats  21120  scmatscm  21122  scmatmulcl  21127  scmatf  21138  mdet1  21210  mdet0  21215  cramerimplem1  21292  cramer  21300  decpmatmul  21380  pmatcollpwscmat  21399  chfacfisf  21462  dv11cn  24598  logbgcd1irr  25372  lnhl  26401  usgrfilem  27109  cplgr3v  27217  wlkreslem  27451  usgr2trlncl  27541  wwlksnextbi  27672  clwwlkccatlem  27767  clwwlkel  27825  clwwlknon1loop  27877  uhgr3cyclex  27961  eucrctshift  28022  1to3vfriswmgr  28059  frgrnbnb  28072  fusgreghash2wspv  28114  numclwwlk6  28169  frgrreggt1  28172  frgrregord013  28174  hhcmpl  28977  upgracycumgr  32400  bj-finsumval0  34570  indexa  35023  founiiun0  41500  or2expropbilem1  43316  fundmdfat  43377  reuopreuprim  43737  elbigolo1  44666  2sphere  44785  itsclquadb  44812