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  1859  sbidm  1900  disamis  2194  r19.28v  2673  fun11uni  5431  fabexg  5559  fores  5605  f1oabexg  5631  fun11iun  5640  fdmeu  5725  fvelrnb  5729  ssimaex  5743  foeqcnvco  5969  f1eqcocnv  5970  isoini  5997  brtposg  6498  tfrcllemssrecs  6596  fiintim  7204  djuex  7347  elni2  7645  dmaddpqlem  7708  nqpi  7709  ltexnqq  7739  nq0nn  7773  nqnq0a  7785  nqnq0m  7786  elnp1st2nd  7807  mullocprlem  7901  cnegexlem3  8466  divmulasscomap  8987  lediv2a  9186  btwnz  9715  eluz2b2  9953  uz2mulcl  9958  eqreznegel  9964  elioo4g  10286  fz0fzelfz0  10483  fz0fzdiffz0  10486  2ffzeq  10497  elfzodifsumelfzo  10568  elfzom1elp1fzo  10569  zpnn0elfzo  10574  infssuzex  10615  ioo0  10643  zmodidfzoimp  10740  expcl2lemap  10937  hashfibclem  11231  iswrdsymb  11267  ccatcl  11306  ccatsymb  11315  swrdfv2  11380  swrdsbslen  11383  swrdspsleq  11384  pfxswrd  11423  pfxccatin12lem3  11449  pfxccatpfx2  11454  swrdccat3blem  11456  reuccatpfxs1  11464  mulreap  11574  redivap  11584  imdivap  11591  caucvgrelemcau  11690  zproddc  12290  fprodseq  12294  p1modz1  12505  negdvdsb  12518  muldvds1  12527  muldvds2  12528  dvdsdivcl  12561  nn0ehalf  12614  nn0oddm1d2  12620  nnoddm1d2  12621  divgcdnn  12696  coprmgcdb  12810  divgcdcoprm0  12823  pw2dvdslemn  12887  oddprmdvds  13077  4sqexercise1  13121  4sqexercise2  13122  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemth  13225  grpissubg  13995  ecqusaddd  14039  ecqusaddcl  14040  rnglz  14173  qusmulrng  14792  quscrng  14793  dvdsrzring  14863  lgsprme0  16027  gausslemma2dlem0e  16038  gausslemma2dlem1a  16043  gausslemma2dlem6  16052  lgsquadlem2  16063  2lgsoddprm  16098  usgrislfuspgrdom  16297  edgssv2en  16306  umgr2edg  16314  uspgredg2v  16328  subupgr  16380  subusgr  16382  vtxdfifiun  16404  eupth2lem3lem3fi  16577