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  4743  f1ocnv  6780  fcdmssb  7060  dfrecs3  8302  odi  8504  snmapen  8970  infcntss  9231  lediv2a  12037  lbreu  12093  nn2ge  12173  dfceil2  13761  leexp1a  14100  faclbnd6  14224  ccatval3  14504  ccatalpha  14518  ccatswrd  14593  pfxccatin12lem2  14655  pfxccat3  14658  pfxccat3a  14662  repsdf2  14702  repswsymball  14703  relexpindlem  14988  dvdsdivcl  16245  nn0ehalf  16307  nn0oddm1d2  16314  nnoddm1d2  16315  sumeven  16316  ndvdssub  16338  coprmgcdb  16578  ncoprmgcdne1b  16579  divgcdcoprm0  16594  ncoprmlnprm  16657  vfermltl  16731  powm2modprm  16733  modprmn0modprm0  16737  dvdsprmpweqle  16816  prmgaplem4  16984  prmgaplem7  16987  cshwshashlem2  17026  efmndid  18780  efmndmnd  18781  gimcnv  19164  cygabl  19788  gsummptnn0fz  19883  rngimcnv  20359  fldidom  20674  lmimcnv  20989  ixpsnbasval  21130  rngqiprngghmlem1  21212  rngqiprngimf  21222  rng2idl1cntr  21230  rngringbdlem1  21231  matbas2  22324  scmatmats  22414  scmatscm  22416  scmatmulcl  22421  scmatf  22432  mdet1  22504  mdet0  22509  cramerimplem1  22586  cramer  22594  decpmatmul  22675  pmatcollpwscmat  22694  chfacfisf  22757  dv11cn  25922  logbgcd1irr  26720  cofcutr  27855  lnhl  28578  usgrfilem  29290  cplgr3v  29398  wlkreslem  29631  usgr2trlncl  29723  wwlksnextbi  29857  clwwlkccatlem  29951  clwwlkel  30008  clwwlknon1loop  30060  uhgr3cyclex  30144  eucrctshift  30205  1to3vfriswmgr  30242  frgrnbnb  30255  fusgreghash2wspv  30297  numclwwlk6  30352  frgrreggt1  30355  frgrregord013  30357  hhcmpl  31162  upgracycumgr  35125  bj-finsumval0  37258  indexa  37712  dmqsblocks  38830  aks6d1c2p2  42092  rimcnv  42490  omord2i  43274  oeord2i  43283  oaun3lem1  43347  founiiun0  45168  or2expropbilem1  47017  fcoresfob  47057  fundmdfat  47114  reuopreuprim  47511  grimedg  47919  grlictr  47991  clnbgr3stgrgrlic  47995  gpgedgvtx1  48037  gpg5nbgrvtx13starlem2  48047  pgnbgreunbgrlem3  48092  pgnbgreunbgrlem6  48098  uspgrsprfo  48120  elbigolo1  48530  2sphere  48722  itsclquadb  48749  lubeldm2  48928  glbeldm2  48929