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  4789  f1ocnv  6860  fcdmssb  7142  dfrecs3  8412  dfrecs3OLD  8413  odi  8617  snmapen  9078  infcntss  9362  lediv2a  12162  lbreu  12218  nn2ge  12293  dfceil2  13879  leexp1a  14215  faclbnd6  14338  ccatval3  14617  ccatalpha  14631  ccatswrd  14706  pfxccatin12lem2  14769  pfxccat3  14772  pfxccat3a  14776  repsdf2  14816  repswsymball  14817  relexpindlem  15102  dvdsdivcl  16353  nn0ehalf  16415  nn0oddm1d2  16422  nnoddm1d2  16423  sumeven  16424  ndvdssub  16446  coprmgcdb  16686  ncoprmgcdne1b  16687  divgcdcoprm0  16702  ncoprmlnprm  16765  vfermltl  16839  powm2modprm  16841  modprmn0modprm0  16845  dvdsprmpweqle  16924  prmgaplem4  17092  prmgaplem7  17095  cshwshashlem2  17134  efmndid  18901  efmndmnd  18902  gimcnv  19285  cygabl  19909  gsummptnn0fz  20004  rngimcnv  20456  fldidom  20771  lmimcnv  21066  ixpsnbasval  21215  rngqiprngghmlem1  21297  rngqiprngimf  21307  rng2idl1cntr  21315  rngringbdlem1  21316  matbas2  22427  scmatmats  22517  scmatscm  22519  scmatmulcl  22524  scmatf  22535  mdet1  22607  mdet0  22612  cramerimplem1  22689  cramer  22697  decpmatmul  22778  pmatcollpwscmat  22797  chfacfisf  22860  dv11cn  26040  logbgcd1irr  26837  cofcutr  27958  lnhl  28623  usgrfilem  29344  cplgr3v  29452  wlkreslem  29687  usgr2trlncl  29780  wwlksnextbi  29914  clwwlkccatlem  30008  clwwlkel  30065  clwwlknon1loop  30117  uhgr3cyclex  30201  eucrctshift  30262  1to3vfriswmgr  30299  frgrnbnb  30312  fusgreghash2wspv  30354  numclwwlk6  30409  frgrreggt1  30412  frgrregord013  30414  hhcmpl  31219  upgracycumgr  35158  bj-finsumval0  37286  indexa  37740  aks6d1c2p2  42120  rimcnv  42527  omord2i  43314  oeord2i  43323  oaun3lem1  43387  founiiun0  45195  or2expropbilem1  47044  fcoresfob  47084  fundmdfat  47141  reuopreuprim  47513  grimedg  47903  grlictr  47975  clnbgr3stgrgrlic  47979  gpgedgvtx1  48020  gpg5nbgrvtx13starlem2  48028  uspgrsprfo  48064  elbigolo1  48478  2sphere  48670  itsclquadb  48697  lubeldm2  48853  glbeldm2  48854