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  406  sylanr1  408  mpan10  478  sbcof2  1863  sbidm  1904  disamis  2198  r19.28v  2679  fun11uni  5449  fabexg  5577  fores  5623  f1oabexg  5649  fun11iun  5658  fdmeu  5743  fvelrnb  5747  ssimaex  5761  foeqcnvco  5990  f1eqcocnv  5991  isoini  6018  brtposg  6519  tfrcllemssrecs  6617  fiintim  7232  djuex  7377  elni2  7675  dmaddpqlem  7738  nqpi  7739  ltexnqq  7769  nq0nn  7803  nqnq0a  7815  nqnq0m  7816  elnp1st2nd  7837  mullocprlem  7931  cnegexlem3  8497  divmulasscomap  9020  lediv2a  9219  btwnz  9748  eluz2b2  9986  uz2mulcl  9991  eqreznegel  9997  elioo4g  10319  fz0fzelfz0  10517  fz0fzdiffz0  10520  2ffzeq  10531  elfzodifsumelfzo  10602  elfzom1elp1fzo  10603  zpnn0elfzo  10608  infssuzex  10649  ioo0  10677  zmodidfzoimp  10774  expcl2lemap  10971  hashfibclem  11265  iswrdsymb  11305  ccatcl  11344  ccatsymb  11353  swrdfv2  11418  swrdsbslen  11421  swrdspsleq  11422  pfxswrd  11461  pfxccatin12lem3  11487  pfxccatpfx2  11492  swrdccat3blem  11494  reuccatpfxs1  11502  mulreap  11612  redivap  11622  imdivap  11629  caucvgrelemcau  11729  zproddc  12329  fprodseq  12333  p1modz1  12544  negdvdsb  12557  muldvds1  12566  muldvds2  12567  dvdsdivcl  12600  nn0ehalf  12653  nn0oddm1d2  12659  nnoddm1d2  12660  divgcdnn  12735  coprmgcdb  12849  divgcdcoprm0  12862  pw2dvdslemn  12926  oddprmdvds  13116  4sqexercise1  13160  4sqexercise2  13161  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemth  13264  grpissubg  13980  ecqusaddd  14024  ecqusaddcl  14025  rnglz  14227  qusmulrng  14852  quscrng  14853  dvdsrzring  14921  lgsprme0  16144  gausslemma2dlem0e  16155  gausslemma2dlem1a  16160  gausslemma2dlem6  16169  lgsquadlem2  16180  2lgsoddprm  16215  usgrislfuspgrdom  16414  edgssv2en  16423  umgr2edg  16431  uspgredg2v  16445  subupgr  16497  subusgr  16499  vtxdfifiun  16521  eupth2lem3lem3fi  16694