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  4742  f1ocnv  6783  fcdmssb  7064  dfrecs3  8301  odi  8503  snmapen  8970  infcntss  9217  lediv2a  12026  lbreu  12082  nn2ge  12162  dfceil2  13753  leexp1a  14092  faclbnd6  14216  ccatval3  14496  ccatalpha  14511  ccatswrd  14586  pfxccatin12lem2  14648  pfxccat3  14651  pfxccat3a  14655  repsdf2  14695  repswsymball  14696  relexpindlem  14980  dvdsdivcl  16237  nn0ehalf  16299  nn0oddm1d2  16306  nnoddm1d2  16307  sumeven  16308  ndvdssub  16330  coprmgcdb  16570  ncoprmgcdne1b  16571  divgcdcoprm0  16586  ncoprmlnprm  16649  vfermltl  16723  powm2modprm  16725  modprmn0modprm0  16729  dvdsprmpweqle  16808  prmgaplem4  16976  prmgaplem7  16979  cshwshashlem2  17018  chnccat  18542  efmndid  18806  efmndmnd  18807  gimcnv  19189  cygabl  19813  gsummptnn0fz  19908  rngimcnv  20384  fldidom  20696  lmimcnv  21011  ixpsnbasval  21152  rngqiprngghmlem1  21234  rngqiprngimf  21244  rng2idl1cntr  21252  rngringbdlem1  21253  matbas2  22346  scmatmats  22436  scmatscm  22438  scmatmulcl  22443  scmatf  22454  mdet1  22526  mdet0  22531  cramerimplem1  22608  cramer  22616  decpmatmul  22697  pmatcollpwscmat  22716  chfacfisf  22779  dv11cn  25943  logbgcd1irr  26741  cofcutr  27878  lnhl  28603  usgrfilem  29316  cplgr3v  29424  wlkreslem  29657  usgr2trlncl  29749  wwlksnextbi  29883  clwwlkccatlem  29980  clwwlkel  30037  clwwlknon1loop  30089  uhgr3cyclex  30173  eucrctshift  30234  1to3vfriswmgr  30271  frgrnbnb  30284  fusgreghash2wspv  30326  numclwwlk6  30381  frgrreggt1  30384  frgrregord013  30386  hhcmpl  31191  upgracycumgr  35208  bj-finsumval0  37340  indexa  37783  dmqsblocks  38961  aks6d1c2p2  42222  rimcnv  42625  omord2i  43408  oeord2i  43417  oaun3lem1  43481  founiiun0  45301  or2expropbilem1  47146  fcoresfob  47186  fundmdfat  47243  reuopreuprim  47640  grimedg  48049  grlictr  48129  clnbgr3stgrgrlim  48133  clnbgr3stgrgrlic  48134  gpgedgvtx1  48176  gpg5nbgrvtx13starlem2  48186  pgnbgreunbgrlem3  48232  pgnbgreunbgrlem6  48238  uspgrsprfo  48262  elbigolo1  48672  2sphere  48864  itsclquadb  48891  lubeldm2  49070  glbeldm2  49071