Theorem anim1ci 627

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 625	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  elpwdifsn  4752  f1ocnv  6823  fcdmssb  7107  dfrecs3  8347  odi  8552  snmapen  9023  infcntss  9270  lediv2a  12100  lbreu  12156  nn2ge  12254  dfceil2  13863  leexp1a  14202  faclbnd6  14326  ccatval3  14606  ccatalpha  14621  ccatswrd  14696  pfxccatin12lem2  14758  pfxccat3  14761  pfxccat3a  14765  repsdf2  14805  repswsymball  14806  relexpindlem  15090  dvdsdivcl  16364  nn0ehalf  16426  nn0oddm1d2  16433  nnoddm1d2  16434  sumeven  16435  ndvdssub  16457  coprmgcdb  16697  ncoprmgcdne1b  16698  divgcdcoprm0  16713  ncoprmlnprm  16777  vfermltl  16851  powm2modprm  16853  modprmn0modprm0  16857  dvdsprmpweqle  16936  prmgaplem4  17104  prmgaplem7  17107  cshwshashlem2  17146  chnccat  18672  efmndid  18937  efmndmnd  18938  gimcnv  19328  cygabl  19952  gsummptnn0fz  20047  rngimcnv  20529  rimcnv  20558  fldidom  20844  lmimcnv  21157  ixpsnbasval  21298  rngqiprngghmlem1  21389  rngqiprngimf  21399  rng2idl1cntr  21407  rngringbdlem1  21408  matbas2  22539  scmatmats  22629  scmatscm  22631  scmatmulcl  22636  scmatf  22647  mdet1  22719  mdet0  22724  cramerimplem1  22801  cramer  22809  decpmatmul  22890  pmatcollpwscmat  22909  chfacfisf  22972  dv11cn  26121  logbgcd1irr  26917  cofcutr  28075  lnhl  28842  elplng  29010  usgrfilem  29586  cplgr3v  29694  wlkreslem  29926  usgr2trlncl  30018  wwlksnextbi  30152  clwwlkccatlem  30249  clwwlkel  30306  clwwlknon1loop  30358  uhgr3cyclex  30442  eucrctshift  30503  1to3vfriswmgr  30540  frgrnbnb  30553  fusgreghash2wspv  30595  numclwwlk6  30650  frgrreggt1  30653  frgrregord013  30655  hhcmpl  31461  upgracycumgr  35516  bj-finsumval0  37789  indexa  38244  dmqsblocks  39478  aks6d1c2p2  42748  omord2i  43890  oeord2i  43899  oaun3lem1  43963  founiiun0  45766  or2expropbilem1  47624  fcoresfob  47664  fundmdfat  47721  reuopreuprim  48130  nprmmul1  48131  ppivalnnprm  48232  grimedg  48555  grlictr  48635  clnbgr3stgrgrlim  48639  clnbgr3stgrgrlic  48640  gpgedgvtx1  48682  gpg5nbgrvtx13starlem2  48692  pgnbgreunbgrlem3  48738  pgnbgreunbgrlem6  48744  uspgrsprfo  48768  elbigolo1  49188  2sphere  49380  itsclquadb  49407  lubeldm2  49585  glbeldm2  49586