Theorem anim1i 340

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
anim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
anim1i	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Proof of Theorem anim1i

Step	Hyp	Ref	Expression
1		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
2		id 19	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	anim12i 338	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  sylanl1  402  sylanr1  404  mpan10  474  sbcof2  1856  sbidm  1897  disamis  2189  r19.28v  2659  fun11uni  5391  fabexg  5515  fores  5560  f1oabexg  5586  fun11iun  5595  fdmeu  5679  fvelrnb  5683  ssimaex  5697  foeqcnvco  5920  f1eqcocnv  5921  isoini  5948  brtposg  6406  tfrcllemssrecs  6504  fiintim  7101  djuex  7218  elni2  7509  dmaddpqlem  7572  nqpi  7573  ltexnqq  7603  nq0nn  7637  nqnq0a  7649  nqnq0m  7650  elnp1st2nd  7671  mullocprlem  7765  cnegexlem3  8331  divmulasscomap  8851  lediv2a  9050  btwnz  9574  eluz2b2  9806  uz2mulcl  9811  eqreznegel  9817  elioo4g  10138  fz0fzelfz0  10331  fz0fzdiffz0  10334  2ffzeq  10345  elfzodifsumelfzo  10415  elfzom1elp1fzo  10416  zpnn0elfzo  10421  infssuzex  10461  ioo0  10487  zmodidfzoimp  10584  expcl2lemap  10781  iswrdsymb  11097  ccatcl  11136  ccatsymb  11145  swrdfv2  11203  swrdsbslen  11206  swrdspsleq  11207  pfxswrd  11246  pfxccatin12lem3  11272  pfxccatpfx2  11277  swrdccat3blem  11279  reuccatpfxs1  11287  mulreap  11383  redivap  11393  imdivap  11400  caucvgrelemcau  11499  zproddc  12098  fprodseq  12102  p1modz1  12313  negdvdsb  12326  muldvds1  12335  muldvds2  12336  dvdsdivcl  12369  nn0ehalf  12422  nn0oddm1d2  12428  nnoddm1d2  12429  divgcdnn  12504  coprmgcdb  12618  divgcdcoprm0  12631  pw2dvdslemn  12695  oddprmdvds  12885  4sqexercise1  12929  4sqexercise2  12930  grpissubg  13739  ecqusaddd  13783  ecqusaddcl  13784  rnglz  13916  qusmulrng  14504  quscrng  14505  dvdsrzring  14575  lgsprme0  15729  gausslemma2dlem0e  15740  gausslemma2dlem1a  15745  gausslemma2dlem6  15754  lgsquadlem2  15765  2lgsoddprm  15800  usgrislfuspgrdom  15996  edgssv2en  16005  umgr2edg  16013  uspgredg2v  16027