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  4765  f1ocnv  6830  fcdmssb  7112  dfrecs3  8386  dfrecs3OLD  8387  odi  8591  snmapen  9052  infcntss  9334  lediv2a  12136  lbreu  12192  nn2ge  12267  dfceil2  13856  leexp1a  14193  faclbnd6  14317  ccatval3  14597  ccatalpha  14611  ccatswrd  14686  pfxccatin12lem2  14749  pfxccat3  14752  pfxccat3a  14756  repsdf2  14796  repswsymball  14797  relexpindlem  15082  dvdsdivcl  16335  nn0ehalf  16397  nn0oddm1d2  16404  nnoddm1d2  16405  sumeven  16406  ndvdssub  16428  coprmgcdb  16668  ncoprmgcdne1b  16669  divgcdcoprm0  16684  ncoprmlnprm  16747  vfermltl  16821  powm2modprm  16823  modprmn0modprm0  16827  dvdsprmpweqle  16906  prmgaplem4  17074  prmgaplem7  17077  cshwshashlem2  17116  efmndid  18866  efmndmnd  18867  gimcnv  19250  cygabl  19872  gsummptnn0fz  19967  rngimcnv  20416  fldidom  20731  lmimcnv  21025  ixpsnbasval  21166  rngqiprngghmlem1  21248  rngqiprngimf  21258  rng2idl1cntr  21266  rngringbdlem1  21267  matbas2  22359  scmatmats  22449  scmatscm  22451  scmatmulcl  22456  scmatf  22467  mdet1  22539  mdet0  22544  cramerimplem1  22621  cramer  22629  decpmatmul  22710  pmatcollpwscmat  22729  chfacfisf  22792  dv11cn  25958  logbgcd1irr  26756  cofcutr  27884  lnhl  28594  usgrfilem  29306  cplgr3v  29414  wlkreslem  29649  usgr2trlncl  29742  wwlksnextbi  29876  clwwlkccatlem  29970  clwwlkel  30027  clwwlknon1loop  30079  uhgr3cyclex  30163  eucrctshift  30224  1to3vfriswmgr  30261  frgrnbnb  30274  fusgreghash2wspv  30316  numclwwlk6  30371  frgrreggt1  30374  frgrregord013  30376  hhcmpl  31181  upgracycumgr  35175  bj-finsumval0  37303  indexa  37757  aks6d1c2p2  42132  rimcnv  42540  omord2i  43325  oeord2i  43334  oaun3lem1  43398  founiiun0  45214  or2expropbilem1  47061  fcoresfob  47101  fundmdfat  47158  reuopreuprim  47540  grimedg  47948  grlictr  48020  clnbgr3stgrgrlic  48024  gpgedgvtx1  48066  gpg5nbgrvtx13starlem2  48074  uspgrsprfo  48123  elbigolo1  48537  2sphere  48729  itsclquadb  48756  lubeldm2  48930  glbeldm2  48931