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  4751  f1ocnv  6837  fcdmssb  7122  dfrecs3  8381  odi  8588  snmapen  9067  infcntss  9315  lediv2a  12212  lbreu  12268  nn2ge  12366  dfceil2  13980  leexp1a  14319  faclbnd6  14444  ccatval3  14725  ccatalpha  14741  ccatswrd  14819  pfxccatin12lem2  14881  pfxccat3  14884  pfxccat3a  14888  repsdf2  14930  repswsymball  14931  relexpindlem  15217  dvdsdivcl  16487  nn0ehalf  16549  nn0oddm1d2  16556  nnoddm1d2  16557  sumeven  16558  ndvdssub  16580  coprmgcdb  16825  ncoprmgcdne1b  16826  divgcdcoprm0  16841  ncoprmlnprm  16905  vfermltl  16980  powm2modprm  16982  modprmn0modprm0  16986  dvdsprmpweqle  17065  prmgaplem4  17233  prmgaplem7  17236  cshwshashlem2  17275  chnccat  18801  mgmn0plusgf  18828  efmndid  19085  efmndmnd  19086  gimcnv  19482  cygabl  20106  gsummptnn0fz  20201  rngimcnv  20687  rimcnv  20718  fldidom  21030  lmimcnv  21343  ixpsnbasval  21484  rngqiprngghmlem1  21584  rngqiprngimf  21594  rng2idl1cntr  21602  rngringbdlem1  21603  matbas2  22737  scmatmats  22827  scmatscm  22829  scmatmulcl  22834  scmatf  22845  mdet1  22917  mdet0  22922  cramerimplem1  23002  cramer  23010  decpmatmul  23091  pmatcollpwscmat  23110  chfacfisf  23173  dv11cn  26322  logbgcd1irr  27123  nna4b4nsq  27991  cofcutr  28311  lnhl  29082  elplng  29259  usgrfilem  29909  cplgr3v  30017  wlkreslem  30249  usgr2trlncl  30347  wwlksnextbi  30484  clwwlkccatlem  30581  clwwlkel  30638  clwwlknon1loop  30690  uhgr3cyclex  30784  eucrctshift  30845  1to3vfriswmgr  30882  frgrnbnb  30895  fusgreghash2wspv  30937  numclwwlk6  30992  frgrreggt1  30995  frgrregord013  30997  hhcmpl  31803  upgracycumgr  35987  bj-finsumval0  38282  indexa  38743  dmqsblocks  39975  aks6d1c2p2  43245  omord2i  44379  oeord2i  44388  oaun3lem1  44452  founiiun0  46281  or2expropbilem1  48178  fcoresfob  48218  fundmdfat  48275  reuopreuprim  48684  nprmmul1  48685  ppivalnnprm  48786  grimedg  49109  grlictr  49189  clnbgr3stgrgrlim  49193  clnbgr3stgrgrlic  49194  gpgedgvtx1  49236  gpg5nbgrvtx13starlem2  49246  pgnbgreunbgrlem3  49292  pgnbgreunbgrlem6  49298  uspgrsprfo  49322  elbigolo1  49745  2sphere  49937  itsclquadb  49964  lubeldm2  50140  glbeldm2  50141