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 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylanl1  406  sylanr1  408  mpan10  478  sbcof2  1863  sbidm  1904  disamis  2198  r19.28v  2679  fun11uni  5451  fabexg  5579  fores  5625  f1oabexg  5651  fun11iun  5660  fdmeu  5746  fvelrnb  5750  ssimaex  5764  foeqcnvco  5996  f1eqcocnv  5997  isoini  6024  brtposg  6525  tfrcllemssrecs  6623  fiintim  7238  djuex  7383  elni2  7681  dmaddpqlem  7744  nqpi  7745  ltexnqq  7775  nq0nn  7809  nqnq0a  7821  nqnq0m  7822  elnp1st2nd  7843  mullocprlem  7937  cnegexlem3  8503  divmulasscomap  9027  lediv2a  9226  btwnz  9767  eluz2b2  10005  uz2mulcl  10010  eqreznegel  10016  elioo4g  10338  fz0fzelfz0  10536  fz0fzdiffz0  10539  2ffzeq  10550  elfzodifsumelfzo  10621  elfzom1elp1fzo  10622  zpnn0elfzo  10627  infssuzex  10668  ioo0  10696  zmodidfzoimp  10793  expcl2lemap  10990  hashfibclem  11284  iswrdsymb  11324  ccatcl  11363  ccatsymb  11372  swrdfv2  11437  swrdsbslen  11440  swrdspsleq  11441  pfxswrd  11480  pfxccatin12lem3  11506  pfxccatpfx2  11511  swrdccat3blem  11513  reuccatpfxs1  11521  mulreap  11631  redivap  11641  imdivap  11648  caucvgrelemcau  11748  zproddc  12348  fprodseq  12352  p1modz1  12563  negdvdsb  12576  muldvds1  12585  muldvds2  12586  dvdsdivcl  12619  nn0ehalf  12672  nn0oddm1d2  12678  nnoddm1d2  12679  divgcdnn  12754  coprmgcdb  12868  divgcdcoprm0  12881  pw2dvdslemn  12945  oddprmdvds  13135  4sqexercise1  13179  4sqexercise2  13180  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemth  13283  grpissubg  13999  ecqusaddd  14043  ecqusaddcl  14044  rnglz  14246  qusmulrng  14871  quscrng  14872  dvdsrzring  14940  bcmono  16124  lgsprme0  16173  gausslemma2dlem0e  16184  gausslemma2dlem1a  16189  gausslemma2dlem6  16198  lgsquadlem2  16209  2lgsoddprm  16244  usgrislfuspgrdom  16443  edgssv2en  16452  umgr2edg  16460  uspgredg2v  16474  subupgr  16526  subusgr  16528  vtxdfifiun  16550  eupth2lem3lem3fi  16723