Theorem anim1ci 628

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

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

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 402

This theorem is used by:  elpwdifsn  4752  f1ocnv  6859  fcdmssb  7146  dfrecs3  8408  odi  8615  snmapen  9094  infcntss  9342  lediv2a  12238  lbreu  12294  nn2ge  12392  dfceil2  14006  leexp1a  14345  faclbnd6  14470  ccatval3  14751  ccatalpha  14767  ccatswrd  14846  pfxccatin12lem2  14908  pfxccat3  14911  pfxccat3a  14915  repsdf2  14957  repswsymball  14958  relexpindlem  15245  dvdsdivcl  16515  nn0ehalf  16577  nn0oddm1d2  16584  nnoddm1d2  16585  sumeven  16586  ndvdssub  16608  coprmgcdb  16853  ncoprmgcdne1b  16854  divgcdcoprm0  16869  ncoprmlnprm  16933  vfermltl  17008  powm2modprm  17010  modprmn0modprm0  17014  dvdsprmpweqle  17093  prmgaplem4  17261  prmgaplem7  17264  cshwshashlem2  17303  chnccat  18829  mgmn0plusgf  18856  efmndid  19113  efmndmnd  19114  gimcnv  19510  cygabl  20135  gsummptnn0fz  20230  rngimcnv  20716  rimcnv  20747  fldidom  21059  lmimcnv  21372  ixpsnbasval  21513  rngqiprngghmlem1  21613  rngqiprngimf  21623  rng2idl1cntr  21631  rngringbdlem1  21632  matbas2  22766  scmatmats  22856  scmatscm  22858  scmatmulcl  22863  scmatf  22874  mdet1  22946  mdet0  22951  cramerimplem1  23031  cramer  23039  decpmatmul  23120  pmatcollpwscmat  23139  chfacfisf  23202  dv11cn  26351  logbgcd1irr  27152  nna4b4nsq  28020  cofcutr  28340  lnhl  29111  elplng  29288  usgrfilem  29938  cplgr3v  30046  wlkreslem  30278  usgr2trlncl  30376  wwlksnextbi  30513  clwwlkccatlem  30610  clwwlkel  30667  clwwlknon1loop  30719  uhgr3cyclex  30813  eucrctshift  30874  1to3vfriswmgr  30911  frgrnbnb  30924  fusgreghash2wspv  30966  numclwwlk6  31021  frgrreggt1  31024  frgrregord013  31026  hhcmpl  31832  jltaleph  36026  upgracycumgr  36075  bj-finsumval0  38398  pibt2  38532  indexa  38859  dmqsblocks  40091  aks6d1c2p2  43361  omord2i  44495  oeord2i  44504  oaun3lem1  44568  founiiun0  46410  or2expropbilem1  48307  fcoresfob  48347  fundmdfat  48404  reuopreuprim  48813  nprmmul1  48814  ppivalnnprm  48915  grimedg  49238  grlictr  49318  clnbgr3stgrgrlim  49322  clnbgr3stgrgrlic  49323  gpgedgvtx1  49365  gpg5nbgrvtx13starlem2  49375  pgnbgreunbgrlem3  49421  pgnbgreunbgrlem6  49427  uspgrsprfo  49451  elbigolo1  49874  2sphere  50066  itsclquadb  50093  lubeldm2  50275  glbeldm2  50276