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  4792  f1ocnv  6845  fcdmssb  7123  dfrecs3  8374  dfrecs3OLD  8375  odi  8581  snmapen  9040  infcntss  9323  lediv2a  12112  lbreu  12168  nn2ge  12243  dfceil2  13808  leexp1a  14144  faclbnd6  14263  ccatval3  14533  ccatalpha  14547  ccatswrd  14622  pfxccatin12lem2  14685  pfxccat3  14688  pfxccat3a  14692  repsdf2  14732  repswsymball  14733  relexpindlem  15014  dvdsdivcl  16263  nn0ehalf  16325  nn0oddm1d2  16332  nnoddm1d2  16333  sumeven  16334  ndvdssub  16356  coprmgcdb  16590  ncoprmgcdne1b  16591  divgcdcoprm0  16606  ncoprmlnprm  16668  vfermltl  16738  powm2modprm  16740  modprmn0modprm0  16744  dvdsprmpweqle  16823  prmgaplem4  16991  prmgaplem7  16994  cshwshashlem2  17034  efmndid  18805  efmndmnd  18806  gimcnv  19181  cygabl  19800  gsummptnn0fz  19895  rngimcnv  20347  lmimcnv  20822  ixpsnbasval  20977  rngqiprngghmlem1  21046  rngqiprngimf  21056  rng2idl1cntr  21064  rngringbdlem1  21065  fldidom  21123  matbas2  22143  scmatmats  22233  scmatscm  22235  scmatmulcl  22240  scmatf  22251  mdet1  22323  mdet0  22328  cramerimplem1  22405  cramer  22413  decpmatmul  22494  pmatcollpwscmat  22513  chfacfisf  22576  dv11cn  25742  logbgcd1irr  26523  cofcutr  27637  lnhl  28121  usgrfilem  28839  cplgr3v  28947  wlkreslem  29181  usgr2trlncl  29272  wwlksnextbi  29403  clwwlkccatlem  29497  clwwlkel  29554  clwwlknon1loop  29606  uhgr3cyclex  29690  eucrctshift  29751  1to3vfriswmgr  29788  frgrnbnb  29801  fusgreghash2wspv  29843  numclwwlk6  29898  frgrreggt1  29901  frgrregord013  29903  hhcmpl  30708  upgracycumgr  34430  bj-finsumval0  36469  indexa  36904  aks6d1c2p2  41263  rimcnv  41396  omord2i  42353  oeord2i  42362  oaun3lem1  42426  founiiun0  44188  or2expropbilem1  46041  fcoresfob  46081  fundmdfat  46136  reuopreuprim  46493  uspgrsprfo  46825  elbigolo1  47331  2sphere  47523  itsclquadb  47550  lubeldm2  47677  glbeldm2  47678