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  1858  sbidm  1899  disamis  2191  r19.28v  2661  fun11uni  5400  fabexg  5524  fores  5569  f1oabexg  5595  fun11iun  5604  fdmeu  5689  fvelrnb  5693  ssimaex  5707  foeqcnvco  5931  f1eqcocnv  5932  isoini  5959  brtposg  6420  tfrcllemssrecs  6518  fiintim  7123  djuex  7242  elni2  7534  dmaddpqlem  7597  nqpi  7598  ltexnqq  7628  nq0nn  7662  nqnq0a  7674  nqnq0m  7675  elnp1st2nd  7696  mullocprlem  7790  cnegexlem3  8356  divmulasscomap  8876  lediv2a  9075  btwnz  9599  eluz2b2  9837  uz2mulcl  9842  eqreznegel  9848  elioo4g  10169  fz0fzelfz0  10362  fz0fzdiffz0  10365  2ffzeq  10376  elfzodifsumelfzo  10447  elfzom1elp1fzo  10448  zpnn0elfzo  10453  infssuzex  10494  ioo0  10520  zmodidfzoimp  10617  expcl2lemap  10814  iswrdsymb  11135  ccatcl  11174  ccatsymb  11183  swrdfv2  11248  swrdsbslen  11251  swrdspsleq  11252  pfxswrd  11291  pfxccatin12lem3  11317  pfxccatpfx2  11322  swrdccat3blem  11324  reuccatpfxs1  11332  mulreap  11429  redivap  11439  imdivap  11446  caucvgrelemcau  11545  zproddc  12145  fprodseq  12149  p1modz1  12360  negdvdsb  12373  muldvds1  12382  muldvds2  12383  dvdsdivcl  12416  nn0ehalf  12469  nn0oddm1d2  12475  nnoddm1d2  12476  divgcdnn  12551  coprmgcdb  12665  divgcdcoprm0  12678  pw2dvdslemn  12742  oddprmdvds  12932  4sqexercise1  12976  4sqexercise2  12977  grpissubg  13786  ecqusaddd  13830  ecqusaddcl  13831  rnglz  13964  qusmulrng  14552  quscrng  14553  dvdsrzring  14623  lgsprme0  15777  gausslemma2dlem0e  15788  gausslemma2dlem1a  15793  gausslemma2dlem6  15802  lgsquadlem2  15813  2lgsoddprm  15848  usgrislfuspgrdom  16047  edgssv2en  16056  umgr2edg  16064  uspgredg2v  16078  subupgr  16130  subusgr  16132  vtxdfifiun  16154  eupth2lem3lem3fi  16327