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  4769  f1ocnv  6840  fcdmssb  7122  dfrecs3  8394  dfrecs3OLD  8395  odi  8599  snmapen  9060  infcntss  9344  lediv2a  12144  lbreu  12200  nn2ge  12275  dfceil2  13861  leexp1a  14197  faclbnd6  14320  ccatval3  14599  ccatalpha  14613  ccatswrd  14688  pfxccatin12lem2  14751  pfxccat3  14754  pfxccat3a  14758  repsdf2  14798  repswsymball  14799  relexpindlem  15084  dvdsdivcl  16335  nn0ehalf  16397  nn0oddm1d2  16404  nnoddm1d2  16405  sumeven  16406  ndvdssub  16428  coprmgcdb  16668  ncoprmgcdne1b  16669  divgcdcoprm0  16684  ncoprmlnprm  16747  vfermltl  16821  powm2modprm  16823  modprmn0modprm0  16827  dvdsprmpweqle  16906  prmgaplem4  17074  prmgaplem7  17077  cshwshashlem2  17116  efmndid  18870  efmndmnd  18871  gimcnv  19254  cygabl  19877  gsummptnn0fz  19972  rngimcnv  20424  fldidom  20739  lmimcnv  21034  ixpsnbasval  21177  rngqiprngghmlem1  21259  rngqiprngimf  21269  rng2idl1cntr  21277  rngringbdlem1  21278  matbas2  22375  scmatmats  22465  scmatscm  22467  scmatmulcl  22472  scmatf  22483  mdet1  22555  mdet0  22560  cramerimplem1  22637  cramer  22645  decpmatmul  22726  pmatcollpwscmat  22745  chfacfisf  22808  dv11cn  25976  logbgcd1irr  26773  cofcutr  27894  lnhl  28559  usgrfilem  29272  cplgr3v  29380  wlkreslem  29615  usgr2trlncl  29708  wwlksnextbi  29842  clwwlkccatlem  29936  clwwlkel  29993  clwwlknon1loop  30045  uhgr3cyclex  30129  eucrctshift  30190  1to3vfriswmgr  30227  frgrnbnb  30240  fusgreghash2wspv  30282  numclwwlk6  30337  frgrreggt1  30340  frgrregord013  30342  hhcmpl  31147  upgracycumgr  35117  bj-finsumval0  37245  indexa  37699  aks6d1c2p2  42079  rimcnv  42490  omord2i  43276  oeord2i  43285  oaun3lem1  43349  founiiun0  45152  or2expropbilem1  47002  fcoresfob  47042  fundmdfat  47099  reuopreuprim  47471  grimedg  47861  grlictr  47933  clnbgr3stgrgrlic  47937  gpgedgvtx1  47978  gpg5nbgrvtx13starlem2  47986  uspgrsprfo  48022  elbigolo1  48436  2sphere  48628  itsclquadb  48655  lubeldm2  48813  glbeldm2  48814