Theorem anim1ci 628

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 23	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	anim12ci 626	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜒 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  elpwdifsn  4755  f1ocnv  6834  fcdmssb  7118  dfrecs3  8364  odi  8569  snmapen  9048  infcntss  9295  lediv2a  12136  lbreu  12192  nn2ge  12290  dfceil2  13902  leexp1a  14241  faclbnd6  14365  ccatval3  14646  ccatalpha  14662  ccatswrd  14740  pfxccatin12lem2  14802  pfxccat3  14805  pfxccat3a  14809  repsdf2  14851  repswsymball  14852  relexpindlem  15138  dvdsdivcl  16410  nn0ehalf  16472  nn0oddm1d2  16479  nnoddm1d2  16480  sumeven  16481  ndvdssub  16503  coprmgcdb  16743  ncoprmgcdne1b  16744  divgcdcoprm0  16759  ncoprmlnprm  16823  vfermltl  16897  powm2modprm  16899  modprmn0modprm0  16903  dvdsprmpweqle  16982  prmgaplem4  17150  prmgaplem7  17153  cshwshashlem2  17192  chnccat  18718  mgmn0plusgf  18745  efmndid  19001  efmndmnd  19002  gimcnv  19398  cygabl  20022  gsummptnn0fz  20117  rngimcnv  20601  rimcnv  20632  fldidom  20942  lmimcnv  21255  ixpsnbasval  21396  rngqiprngghmlem1  21494  rngqiprngimf  21504  rng2idl1cntr  21512  rngringbdlem1  21513  matbas2  22647  scmatmats  22737  scmatscm  22739  scmatmulcl  22744  scmatf  22755  mdet1  22827  mdet0  22832  cramerimplem1  22912  cramer  22920  decpmatmul  23001  pmatcollpwscmat  23020  chfacfisf  23083  dv11cn  26233  logbgcd1irr  27032  cofcutr  28190  lnhl  28961  elplng  29138  usgrfilem  29788  cplgr3v  29896  wlkreslem  30128  usgr2trlncl  30226  wwlksnextbi  30363  clwwlkccatlem  30460  clwwlkel  30517  clwwlknon1loop  30569  uhgr3cyclex  30663  eucrctshift  30724  1to3vfriswmgr  30761  frgrnbnb  30774  fusgreghash2wspv  30816  numclwwlk6  30871  frgrreggt1  30874  frgrregord013  30876  hhcmpl  31682  upgracycumgr  35734  bj-finsumval0  38039  indexa  38485  dmqsblocks  39717  aks6d1c2p2  42987  omord2i  44144  oeord2i  44153  oaun3lem1  44217  founiiun0  46024  or2expropbilem1  47922  fcoresfob  47962  fundmdfat  48019  reuopreuprim  48428  nprmmul1  48429  ppivalnnprm  48530  grimedg  48853  grlictr  48933  clnbgr3stgrgrlim  48937  clnbgr3stgrgrlic  48938  gpgedgvtx1  48980  gpg5nbgrvtx13starlem2  48990  pgnbgreunbgrlem3  49036  pgnbgreunbgrlem6  49042  uspgrsprfo  49066  elbigolo1  49489  2sphere  49681  itsclquadb  49708  lubeldm2  49884  glbeldm2  49885