Theorem anim1ci 617

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 615	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  4746  f1ocnv  6787  fcdmssb  7069  dfrecs3  8306  odi  8508  snmapen  8979  infcntss  9227  lediv2a  12040  lbreu  12096  nn2ge  12176  dfceil2  13763  leexp1a  14102  faclbnd6  14226  ccatval3  14506  ccatalpha  14521  ccatswrd  14596  pfxccatin12lem2  14658  pfxccat3  14661  pfxccat3a  14665  repsdf2  14705  repswsymball  14706  relexpindlem  14990  dvdsdivcl  16247  nn0ehalf  16309  nn0oddm1d2  16316  nnoddm1d2  16317  sumeven  16318  ndvdssub  16340  coprmgcdb  16580  ncoprmgcdne1b  16581  divgcdcoprm0  16596  ncoprmlnprm  16659  vfermltl  16733  powm2modprm  16735  modprmn0modprm0  16739  dvdsprmpweqle  16818  prmgaplem4  16986  prmgaplem7  16989  cshwshashlem2  17028  chnccat  18553  efmndid  18817  efmndmnd  18818  gimcnv  19200  cygabl  19824  gsummptnn0fz  19919  rngimcnv  20396  fldidom  20708  lmimcnv  21023  ixpsnbasval  21164  rngqiprngghmlem1  21246  rngqiprngimf  21256  rng2idl1cntr  21264  rngringbdlem1  21265  matbas2  22369  scmatmats  22459  scmatscm  22461  scmatmulcl  22466  scmatf  22477  mdet1  22549  mdet0  22554  cramerimplem1  22631  cramer  22639  decpmatmul  22720  pmatcollpwscmat  22739  chfacfisf  22802  dv11cn  25966  logbgcd1irr  26764  cofcutr  27906  lnhl  28670  usgrfilem  29383  cplgr3v  29491  wlkreslem  29724  usgr2trlncl  29816  wwlksnextbi  29950  clwwlkccatlem  30047  clwwlkel  30104  clwwlknon1loop  30156  uhgr3cyclex  30240  eucrctshift  30301  1to3vfriswmgr  30338  frgrnbnb  30351  fusgreghash2wspv  30393  numclwwlk6  30448  frgrreggt1  30451  frgrregord013  30453  hhcmpl  31258  upgracycumgr  35328  bj-finsumval0  37461  indexa  37905  dmqsblocks  39139  aks6d1c2p2  42410  rimcnv  42808  omord2i  43579  oeord2i  43588  oaun3lem1  43652  founiiun0  45470  or2expropbilem1  47314  fcoresfob  47354  fundmdfat  47411  reuopreuprim  47808  grimedg  48217  grlictr  48297  clnbgr3stgrgrlim  48301  clnbgr3stgrgrlic  48302  gpgedgvtx1  48344  gpg5nbgrvtx13starlem2  48354  pgnbgreunbgrlem3  48400  pgnbgreunbgrlem6  48406  uspgrsprfo  48430  elbigolo1  48839  2sphere  49031  itsclquadb  49058  lubeldm2  49237  glbeldm2  49238