Theorem anim1ci 616

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 614	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  4793  f1ocnv  6860  fcdmssb  7141  dfrecs3  8410  dfrecs3OLD  8411  odi  8615  snmapen  9076  infcntss  9359  lediv2a  12159  lbreu  12215  nn2ge  12290  dfceil2  13875  leexp1a  14211  faclbnd6  14334  ccatval3  14613  ccatalpha  14627  ccatswrd  14702  pfxccatin12lem2  14765  pfxccat3  14768  pfxccat3a  14772  repsdf2  14812  repswsymball  14813  relexpindlem  15098  dvdsdivcl  16349  nn0ehalf  16411  nn0oddm1d2  16418  nnoddm1d2  16419  sumeven  16420  ndvdssub  16442  coprmgcdb  16682  ncoprmgcdne1b  16683  divgcdcoprm0  16698  ncoprmlnprm  16761  vfermltl  16834  powm2modprm  16836  modprmn0modprm0  16840  dvdsprmpweqle  16919  prmgaplem4  17087  prmgaplem7  17090  cshwshashlem2  17130  efmndid  18913  efmndmnd  18914  gimcnv  19297  cygabl  19923  gsummptnn0fz  20018  rngimcnv  20472  fldidom  20787  lmimcnv  21083  ixpsnbasval  21232  rngqiprngghmlem1  21314  rngqiprngimf  21324  rng2idl1cntr  21332  rngringbdlem1  21333  matbas2  22442  scmatmats  22532  scmatscm  22534  scmatmulcl  22539  scmatf  22550  mdet1  22622  mdet0  22627  cramerimplem1  22704  cramer  22712  decpmatmul  22793  pmatcollpwscmat  22812  chfacfisf  22875  dv11cn  26054  logbgcd1irr  26851  cofcutr  27972  lnhl  28637  usgrfilem  29358  cplgr3v  29466  wlkreslem  29701  usgr2trlncl  29792  wwlksnextbi  29923  clwwlkccatlem  30017  clwwlkel  30074  clwwlknon1loop  30126  uhgr3cyclex  30210  eucrctshift  30271  1to3vfriswmgr  30308  frgrnbnb  30321  fusgreghash2wspv  30363  numclwwlk6  30418  frgrreggt1  30421  frgrregord013  30423  hhcmpl  31228  upgracycumgr  35137  bj-finsumval0  37267  indexa  37719  aks6d1c2p2  42100  rimcnv  42503  omord2i  43290  oeord2i  43299  oaun3lem1  43363  founiiun0  45132  or2expropbilem1  46981  fcoresfob  47021  fundmdfat  47078  reuopreuprim  47450  grimedg  47840  grlictr  47910  clnbgr3stgrgrlic  47914  gpgedgvtx1  47954  gpg5nbgrvtx13starlem2  47962  uspgrsprfo  47991  elbigolo1  48406  2sphere  48598  itsclquadb  48625  lubeldm2  48752  glbeldm2  48753