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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  elpwdifsn  4756  f1ocnv  6833  fcdmssb  7117  dfrecs3  8357  odi  8562  snmapen  9033  infcntss  9280  lediv2a  12115  lbreu  12171  nn2ge  12269  dfceil2  13879  leexp1a  14218  faclbnd6  14342  ccatval3  14623  ccatalpha  14638  ccatswrd  14713  pfxccatin12lem2  14775  pfxccat3  14778  pfxccat3a  14782  repsdf2  14822  repswsymball  14823  relexpindlem  15107  dvdsdivcl  16380  nn0ehalf  16442  nn0oddm1d2  16449  nnoddm1d2  16450  sumeven  16451  ndvdssub  16473  coprmgcdb  16713  ncoprmgcdne1b  16714  divgcdcoprm0  16729  ncoprmlnprm  16793  vfermltl  16867  powm2modprm  16869  modprmn0modprm0  16873  dvdsprmpweqle  16952  prmgaplem4  17120  prmgaplem7  17123  cshwshashlem2  17162  chnccat  18688  efmndid  18953  efmndmnd  18954  gimcnv  19343  cygabl  19967  gsummptnn0fz  20062  rngimcnv  20545  rimcnv  20576  fldidom  20886  lmimcnv  21199  ixpsnbasval  21340  rngqiprngghmlem1  21438  rngqiprngimf  21448  rng2idl1cntr  21456  rngringbdlem1  21457  matbas2  22589  scmatmats  22679  scmatscm  22681  scmatmulcl  22686  scmatf  22697  mdet1  22769  mdet0  22774  cramerimplem1  22851  cramer  22859  decpmatmul  22940  pmatcollpwscmat  22959  chfacfisf  23022  dv11cn  26171  logbgcd1irr  26970  cofcutr  28128  lnhl  28898  elplng  29073  usgrfilem  29688  cplgr3v  29796  wlkreslem  30028  usgr2trlncl  30120  wwlksnextbi  30254  clwwlkccatlem  30351  clwwlkel  30408  clwwlknon1loop  30460  uhgr3cyclex  30544  eucrctshift  30605  1to3vfriswmgr  30642  frgrnbnb  30655  fusgreghash2wspv  30697  numclwwlk6  30752  frgrreggt1  30755  frgrregord013  30757  hhcmpl  31563  upgracycumgr  35653  bj-finsumval0  37957  indexa  38412  dmqsblocks  39644  aks6d1c2p2  42914  omord2i  44056  oeord2i  44065  oaun3lem1  44129  founiiun0  45936  or2expropbilem1  47797  fcoresfob  47837  fundmdfat  47894  reuopreuprim  48303  nprmmul1  48304  ppivalnnprm  48405  grimedg  48728  grlictr  48808  clnbgr3stgrgrlim  48812  clnbgr3stgrgrlic  48813  gpgedgvtx1  48855  gpg5nbgrvtx13starlem2  48865  pgnbgreunbgrlem3  48911  pgnbgreunbgrlem6  48917  uspgrsprfo  48941  elbigolo1  49365  2sphere  49557  itsclquadb  49584  lubeldm2  49762  glbeldm2  49763