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  1810  sbidm  1851  disamis  2137  r19.28v  2605  fun11uni  5287  fabexg  5404  fores  5448  f1oabexg  5474  fun11iun  5483  fvelrnb  5564  ssimaex  5578  foeqcnvco  5791  f1eqcocnv  5792  isoini  5819  brtposg  6255  tfrcllemssrecs  6353  fiintim  6928  djuex  7042  elni2  7313  dmaddpqlem  7376  nqpi  7377  ltexnqq  7407  nq0nn  7441  nqnq0a  7453  nqnq0m  7454  elnp1st2nd  7475  mullocprlem  7569  cnegexlem3  8134  divmulasscomap  8653  lediv2a  8852  btwnz  9372  eluz2b2  9603  uz2mulcl  9608  eqreznegel  9614  elioo4g  9934  fz0fzelfz0  10127  fz0fzdiffz0  10130  2ffzeq  10141  elfzodifsumelfzo  10201  elfzom1elp1fzo  10202  zpnn0elfzo  10207  ioo0  10260  zmodidfzoimp  10354  expcl2lemap  10532  mulreap  10873  redivap  10883  imdivap  10890  caucvgrelemcau  10989  zproddc  11587  fprodseq  11591  p1modz1  11801  negdvdsb  11814  muldvds1  11823  muldvds2  11824  dvdsdivcl  11856  nn0ehalf  11908  nn0oddm1d2  11914  nnoddm1d2  11915  infssuzex  11950  divgcdnn  11976  coprmgcdb  12088  divgcdcoprm0  12101  pw2dvdslemn  12165  oddprmdvds  12352  grpissubg  13054  dvdsrzring  13496  lgsprme0  14446