Theorem anim1ci 609

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  elpwdifsn  4552  f1ocnv  6403  frnssb  6655  dfrecs3  7752  odi  7943  snmapen  8322  infcntss  8522  lediv2a  11271  lbreu  11327  nn2ge  11403  dfceil2  12959  leexp1a  13237  faclbnd6  13404  ccatval3  13669  ccatalpha  13683  ccatpfx  13810  pfxccatin12lem2  13858  pfxccat3  13863  pfxccat3a  13869  repsdf2  13924  repswsymball  13925  dvdsdivcl  15445  nn0ehalf  15508  nn0oddm1d2  15515  nnoddm1d2  15516  sumeven  15517  ndvdssub  15539  coprmgcdb  15768  ncoprmgcdne1b  15769  divgcdcoprm0  15784  ncoprmlnprm  15840  vfermltl  15910  powm2modprm  15912  modprmn0modprm0  15916  dvdsprmpweqle  15994  prmgaplem4  16162  prmgaplem7  16165  cshwshashlem2  16202  logbgcd1irr  24972  wlkreslem  27018  wwlksnextbi  27255  hhcmpl  28629  elbigolo1  43348  2sphere  43467  itsclquadb  43494