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 396

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 206  df-an 397

This theorem is referenced by:  elpwdifsn  4791  f1ocnv  6842  fcdmssb  7117  dfrecs3  8368  dfrecs3OLD  8369  odi  8575  snmapen  9034  infcntss  9317  lediv2a  12104  lbreu  12160  nn2ge  12235  dfceil2  13800  leexp1a  14136  faclbnd6  14255  ccatval3  14525  ccatalpha  14539  ccatswrd  14614  pfxccatin12lem2  14677  pfxccat3  14680  pfxccat3a  14684  repsdf2  14724  repswsymball  14725  relexpindlem  15006  dvdsdivcl  16255  nn0ehalf  16317  nn0oddm1d2  16324  nnoddm1d2  16325  sumeven  16326  ndvdssub  16348  coprmgcdb  16582  ncoprmgcdne1b  16583  divgcdcoprm0  16598  ncoprmlnprm  16660  vfermltl  16730  powm2modprm  16732  modprmn0modprm0  16736  dvdsprmpweqle  16815  prmgaplem4  16983  prmgaplem7  16986  cshwshashlem2  17026  efmndid  18765  efmndmnd  18766  gimcnv  19135  cygabl  19753  gsummptnn0fz  19848  lmimcnv  20670  ixpsnbasval  20824  fldidom  20915  matbas2  21914  scmatmats  22004  scmatscm  22006  scmatmulcl  22011  scmatf  22022  mdet1  22094  mdet0  22099  cramerimplem1  22176  cramer  22184  decpmatmul  22265  pmatcollpwscmat  22284  chfacfisf  22347  dv11cn  25509  logbgcd1irr  26288  cofcutr  27400  lnhl  27855  usgrfilem  28573  cplgr3v  28681  wlkreslem  28915  usgr2trlncl  29006  wwlksnextbi  29137  clwwlkccatlem  29231  clwwlkel  29288  clwwlknon1loop  29340  uhgr3cyclex  29424  eucrctshift  29485  1to3vfriswmgr  29522  frgrnbnb  29535  fusgreghash2wspv  29577  numclwwlk6  29632  frgrreggt1  29635  frgrregord013  29637  hhcmpl  30440  upgracycumgr  34132  bj-finsumval0  36154  indexa  36589  aks6d1c2p2  40945  rimcnv  41089  omord2i  42036  oeord2i  42045  oaun3lem1  42109  founiiun0  43873  or2expropbilem1  45728  fcoresfob  45768  fundmdfat  45823  reuopreuprim  46180  uspgrsprfo  46512  rngimcnv  46690  rngqiprngghmlem1  46752  rngqiprngimf  46762  rng2idl1cntr  46770  rngringbdlem1  46771  elbigolo1  47196  2sphere  47388  itsclquadb  47415  lubeldm2  47542  glbeldm2  47543