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 207  df-an 396

This theorem is referenced by:  elpwdifsn  4814  f1ocnv  6874  fcdmssb  7156  dfrecs3  8428  dfrecs3OLD  8429  odi  8635  snmapen  9103  infcntss  9390  lediv2a  12189  lbreu  12245  nn2ge  12320  dfceil2  13890  leexp1a  14225  faclbnd6  14348  ccatval3  14627  ccatalpha  14641  ccatswrd  14716  pfxccatin12lem2  14779  pfxccat3  14782  pfxccat3a  14786  repsdf2  14826  repswsymball  14827  relexpindlem  15112  dvdsdivcl  16364  nn0ehalf  16426  nn0oddm1d2  16433  nnoddm1d2  16434  sumeven  16435  ndvdssub  16457  coprmgcdb  16696  ncoprmgcdne1b  16697  divgcdcoprm0  16712  ncoprmlnprm  16775  vfermltl  16848  powm2modprm  16850  modprmn0modprm0  16854  dvdsprmpweqle  16933  prmgaplem4  17101  prmgaplem7  17104  cshwshashlem2  17144  efmndid  18923  efmndmnd  18924  gimcnv  19307  cygabl  19933  gsummptnn0fz  20028  rngimcnv  20482  fldidom  20793  lmimcnv  21089  ixpsnbasval  21238  rngqiprngghmlem1  21320  rngqiprngimf  21330  rng2idl1cntr  21338  rngringbdlem1  21339  matbas2  22448  scmatmats  22538  scmatscm  22540  scmatmulcl  22545  scmatf  22556  mdet1  22628  mdet0  22633  cramerimplem1  22710  cramer  22718  decpmatmul  22799  pmatcollpwscmat  22818  chfacfisf  22881  dv11cn  26060  logbgcd1irr  26855  cofcutr  27976  lnhl  28641  usgrfilem  29362  cplgr3v  29470  wlkreslem  29705  usgr2trlncl  29796  wwlksnextbi  29927  clwwlkccatlem  30021  clwwlkel  30078  clwwlknon1loop  30130  uhgr3cyclex  30214  eucrctshift  30275  1to3vfriswmgr  30312  frgrnbnb  30325  fusgreghash2wspv  30367  numclwwlk6  30422  frgrreggt1  30425  frgrregord013  30427  hhcmpl  31232  upgracycumgr  35121  bj-finsumval0  37251  indexa  37693  aks6d1c2p2  42076  rimcnv  42472  omord2i  43263  oeord2i  43272  oaun3lem1  43336  founiiun0  45097  or2expropbilem1  46947  fcoresfob  46987  fundmdfat  47044  reuopreuprim  47400  grimedg  47787  grlictr  47832  uspgrsprfo  47871  elbigolo1  48291  2sphere  48483  itsclquadb  48510  lubeldm2  48636  glbeldm2  48637