Theorem anim1ci 617

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 615	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  4735  f1ocnv  6793  fcdmssb  7075  dfrecs3  8312  odi  8514  snmapen  8985  infcntss  9233  lediv2a  12050  lbreu  12106  nn2ge  12204  dfceil2  13798  leexp1a  14137  faclbnd6  14261  ccatval3  14541  ccatalpha  14556  ccatswrd  14631  pfxccatin12lem2  14693  pfxccat3  14696  pfxccat3a  14700  repsdf2  14740  repswsymball  14741  relexpindlem  15025  dvdsdivcl  16285  nn0ehalf  16347  nn0oddm1d2  16354  nnoddm1d2  16355  sumeven  16356  ndvdssub  16378  coprmgcdb  16618  ncoprmgcdne1b  16619  divgcdcoprm0  16634  ncoprmlnprm  16698  vfermltl  16772  powm2modprm  16774  modprmn0modprm0  16778  dvdsprmpweqle  16857  prmgaplem4  17025  prmgaplem7  17028  cshwshashlem2  17067  chnccat  18592  efmndid  18856  efmndmnd  18857  gimcnv  19242  cygabl  19866  gsummptnn0fz  19961  rngimcnv  20436  fldidom  20748  lmimcnv  21062  ixpsnbasval  21203  rngqiprngghmlem1  21285  rngqiprngimf  21295  rng2idl1cntr  21303  rngringbdlem1  21304  matbas2  22386  scmatmats  22476  scmatscm  22478  scmatmulcl  22483  scmatf  22494  mdet1  22566  mdet0  22571  cramerimplem1  22648  cramer  22656  decpmatmul  22737  pmatcollpwscmat  22756  chfacfisf  22819  dv11cn  25968  logbgcd1irr  26758  cofcutr  27916  lnhl  28683  usgrfilem  29396  cplgr3v  29504  wlkreslem  29736  usgr2trlncl  29828  wwlksnextbi  29962  clwwlkccatlem  30059  clwwlkel  30116  clwwlknon1loop  30168  uhgr3cyclex  30252  eucrctshift  30313  1to3vfriswmgr  30350  frgrnbnb  30363  fusgreghash2wspv  30405  numclwwlk6  30460  frgrreggt1  30463  frgrregord013  30465  hhcmpl  31271  upgracycumgr  35335  bj-finsumval0  37599  indexa  38054  dmqsblocks  39288  aks6d1c2p2  42558  rimcnv  42962  omord2i  43729  oeord2i  43738  oaun3lem1  43802  founiiun0  45620  or2expropbilem1  47474  fcoresfob  47514  fundmdfat  47571  reuopreuprim  47980  nprmmul1  47981  ppivalnnprm  48082  grimedg  48405  grlictr  48485  clnbgr3stgrgrlim  48489  clnbgr3stgrgrlic  48490  gpgedgvtx1  48532  gpg5nbgrvtx13starlem2  48542  pgnbgreunbgrlem3  48588  pgnbgreunbgrlem6  48594  uspgrsprfo  48618  elbigolo1  49027  2sphere  49219  itsclquadb  49246  lubeldm2  49425  glbeldm2  49426