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  5288  fabexg  5405  fores  5449  f1oabexg  5475  fun11iun  5484  fvelrnb  5566  ssimaex  5580  foeqcnvco  5794  f1eqcocnv  5795  isoini  5822  brtposg  6258  tfrcllemssrecs  6356  fiintim  6931  djuex  7045  elni2  7316  dmaddpqlem  7379  nqpi  7380  ltexnqq  7410  nq0nn  7444  nqnq0a  7456  nqnq0m  7457  elnp1st2nd  7478  mullocprlem  7572  cnegexlem3  8137  divmulasscomap  8656  lediv2a  8855  btwnz  9375  eluz2b2  9606  uz2mulcl  9611  eqreznegel  9617  elioo4g  9937  fz0fzelfz0  10130  fz0fzdiffz0  10133  2ffzeq  10144  elfzodifsumelfzo  10204  elfzom1elp1fzo  10205  zpnn0elfzo  10210  ioo0  10263  zmodidfzoimp  10357  expcl2lemap  10535  mulreap  10876  redivap  10886  imdivap  10893  caucvgrelemcau  10992  zproddc  11590  fprodseq  11594  p1modz1  11804  negdvdsb  11817  muldvds1  11826  muldvds2  11827  dvdsdivcl  11859  nn0ehalf  11911  nn0oddm1d2  11917  nnoddm1d2  11918  infssuzex  11953  divgcdnn  11979  coprmgcdb  12091  divgcdcoprm0  12104  pw2dvdslemn  12168  oddprmdvds  12355  grpissubg  13068  rnglz  13171  dvdsrzring  13667  lgsprme0  14631