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  1834  sbidm  1875  disamis  2166  r19.28v  2635  fun11uni  5350  fabexg  5472  fores  5517  f1oabexg  5543  fun11iun  5552  fvelrnb  5636  ssimaex  5650  foeqcnvco  5869  f1eqcocnv  5870  isoini  5897  brtposg  6350  tfrcllemssrecs  6448  fiintim  7040  djuex  7157  elni2  7440  dmaddpqlem  7503  nqpi  7504  ltexnqq  7534  nq0nn  7568  nqnq0a  7580  nqnq0m  7581  elnp1st2nd  7602  mullocprlem  7696  cnegexlem3  8262  divmulasscomap  8782  lediv2a  8981  btwnz  9505  eluz2b2  9737  uz2mulcl  9742  eqreznegel  9748  elioo4g  10069  fz0fzelfz0  10262  fz0fzdiffz0  10265  2ffzeq  10276  elfzodifsumelfzo  10343  elfzom1elp1fzo  10344  zpnn0elfzo  10349  infssuzex  10389  ioo0  10415  zmodidfzoimp  10512  expcl2lemap  10709  iswrdsymb  11025  ccatcl  11063  ccatsymb  11072  swrdfv2  11130  swrdsbslen  11133  swrdspsleq  11134  pfxswrd  11171  mulreap  11225  redivap  11235  imdivap  11242  caucvgrelemcau  11341  zproddc  11940  fprodseq  11944  p1modz1  12155  negdvdsb  12168  muldvds1  12177  muldvds2  12178  dvdsdivcl  12211  nn0ehalf  12264  nn0oddm1d2  12270  nnoddm1d2  12271  divgcdnn  12346  coprmgcdb  12460  divgcdcoprm0  12473  pw2dvdslemn  12537  oddprmdvds  12727  4sqexercise1  12771  4sqexercise2  12772  grpissubg  13580  ecqusaddd  13624  ecqusaddcl  13625  rnglz  13757  qusmulrng  14344  quscrng  14345  dvdsrzring  14415  lgsprme0  15569  gausslemma2dlem0e  15580  gausslemma2dlem1a  15585  gausslemma2dlem6  15594  lgsquadlem2  15605  2lgsoddprm  15640