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 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  4756  f1ocnv  6815  fcdmssb  7097  dfrecs3  8344  odi  8546  snmapen  9012  infcntss  9280  lediv2a  12084  lbreu  12140  nn2ge  12220  dfceil2  13808  leexp1a  14147  faclbnd6  14271  ccatval3  14551  ccatalpha  14565  ccatswrd  14640  pfxccatin12lem2  14703  pfxccat3  14706  pfxccat3a  14710  repsdf2  14750  repswsymball  14751  relexpindlem  15036  dvdsdivcl  16293  nn0ehalf  16355  nn0oddm1d2  16362  nnoddm1d2  16363  sumeven  16364  ndvdssub  16386  coprmgcdb  16626  ncoprmgcdne1b  16627  divgcdcoprm0  16642  ncoprmlnprm  16705  vfermltl  16779  powm2modprm  16781  modprmn0modprm0  16785  dvdsprmpweqle  16864  prmgaplem4  17032  prmgaplem7  17035  cshwshashlem2  17074  efmndid  18822  efmndmnd  18823  gimcnv  19206  cygabl  19828  gsummptnn0fz  19923  rngimcnv  20372  fldidom  20687  lmimcnv  20981  ixpsnbasval  21122  rngqiprngghmlem1  21204  rngqiprngimf  21214  rng2idl1cntr  21222  rngringbdlem1  21223  matbas2  22315  scmatmats  22405  scmatscm  22407  scmatmulcl  22412  scmatf  22423  mdet1  22495  mdet0  22500  cramerimplem1  22577  cramer  22585  decpmatmul  22666  pmatcollpwscmat  22685  chfacfisf  22748  dv11cn  25913  logbgcd1irr  26711  cofcutr  27839  lnhl  28549  usgrfilem  29261  cplgr3v  29369  wlkreslem  29604  usgr2trlncl  29697  wwlksnextbi  29831  clwwlkccatlem  29925  clwwlkel  29982  clwwlknon1loop  30034  uhgr3cyclex  30118  eucrctshift  30179  1to3vfriswmgr  30216  frgrnbnb  30229  fusgreghash2wspv  30271  numclwwlk6  30326  frgrreggt1  30329  frgrregord013  30331  hhcmpl  31136  upgracycumgr  35147  bj-finsumval0  37280  indexa  37734  dmqsblocks  38852  aks6d1c2p2  42114  rimcnv  42512  omord2i  43297  oeord2i  43306  oaun3lem1  43370  founiiun0  45191  or2expropbilem1  47037  fcoresfob  47077  fundmdfat  47134  reuopreuprim  47531  grimedg  47939  grlictr  48011  clnbgr3stgrgrlic  48015  gpgedgvtx1  48057  gpg5nbgrvtx13starlem2  48067  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  uspgrsprfo  48140  elbigolo1  48550  2sphere  48742  itsclquadb  48769  lubeldm2  48948  glbeldm2  48949