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:  norassOLD  1536  elpwdifsn  4719  f1ocnv  6712  frnssb  6977  dfrecs3  8174  dfrecs3OLD  8175  odi  8372  snmapen  8782  infcntss  9018  lediv2a  11799  lbreu  11855  nn2ge  11930  dfceil2  13487  leexp1a  13821  faclbnd6  13941  ccatval3  14212  ccatalpha  14226  ccatswrd  14309  pfxccatin12lem2  14372  pfxccat3  14375  pfxccat3a  14379  repsdf2  14419  repswsymball  14420  relexpindlem  14702  dvdsdivcl  15953  nn0ehalf  16015  nn0oddm1d2  16022  nnoddm1d2  16023  sumeven  16024  ndvdssub  16046  coprmgcdb  16282  ncoprmgcdne1b  16283  divgcdcoprm0  16298  ncoprmlnprm  16360  vfermltl  16430  powm2modprm  16432  modprmn0modprm0  16436  dvdsprmpweqle  16515  prmgaplem4  16683  prmgaplem7  16686  cshwshashlem2  16726  efmndid  18442  efmndmnd  18443  gimcnv  18798  cygabl  19406  gsummptnn0fz  19502  lmimcnv  20244  ixpsnbasval  20393  fldidom  20489  matbas2  21478  scmatmats  21568  scmatscm  21570  scmatmulcl  21575  scmatf  21586  mdet1  21658  mdet0  21663  cramerimplem1  21740  cramer  21748  decpmatmul  21829  pmatcollpwscmat  21848  chfacfisf  21911  dv11cn  25070  logbgcd1irr  25849  lnhl  26880  usgrfilem  27597  cplgr3v  27705  wlkreslem  27939  usgr2trlncl  28029  wwlksnextbi  28160  clwwlkccatlem  28254  clwwlkel  28311  clwwlknon1loop  28363  uhgr3cyclex  28447  eucrctshift  28508  1to3vfriswmgr  28545  frgrnbnb  28558  fusgreghash2wspv  28600  numclwwlk6  28655  frgrreggt1  28658  frgrregord013  28660  hhcmpl  29463  upgracycumgr  33015  cofcutr  34019  bj-finsumval0  35383  indexa  35818  founiiun0  42617  or2expropbilem1  44413  fcoresfob  44453  fundmdfat  44508  reuopreuprim  44866  uspgrsprfo  45198  elbigolo1  45791  2sphere  45983  itsclquadb  46010  lubeldm2  46138  glbeldm2  46139