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  5454  fabexg  5582  fores  5628  f1oabexg  5654  fun11iun  5663  fdmeu  5749  fvelrnb  5753  ssimaex  5767  foeqcnvco  5999  f1eqcocnv  6000  isoini  6027  brtposg  6530  tfrcllemssrecs  6628  fiintim  7244  djuex  7390  elni2  7688  dmaddpqlem  7751  nqpi  7752  ltexnqq  7782  nq0nn  7816  nqnq0a  7828  nqnq0m  7829  elnp1st2nd  7850  mullocprlem  7944  cnegexlem3  8511  divmulasscomap  9035  lediv2a  9234  btwnz  9776  eluz2b2  10019  uz2mulcl  10024  eqreznegel  10030  elioo4g  10353  fz0fzelfz0  10551  fz0fzdiffz0  10554  2ffzeq  10565  elfzodifsumelfzo  10636  elfzom1elp1fzo  10637  zpnn0elfzo  10642  infssuzex  10683  ioo0  10711  zmodidfzoimp  10812  expcl2lemap  11009  hashfibclem  11304  iswrdsymb  11344  ccatcl  11383  ccatsymb  11392  swrdfv2  11457  swrdsbslen  11460  swrdspsleq  11461  pfxswrd  11500  pfxccatin12lem3  11526  pfxccatpfx2  11531  swrdccat3blem  11533  reuccatpfxs1  11541  mulreap  11651  redivap  11661  imdivap  11668  caucvgrelemcau  11768  zproddc  12371  fprodseq  12375  p1modz1  12586  negdvdsb  12599  muldvds1  12608  muldvds2  12609  dvdsdivcl  12642  nn0ehalf  12695  nn0oddm1d2  12701  nnoddm1d2  12702  divgcdnn  12777  coprmgcdb  12891  divgcdcoprm0  12904  pwbdvdslemn  12969  oddprmdvds  13162  4sqexercise1  13206  4sqexercise2  13207  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemth  13339  grpissubg  14056  ecqusaddd  14100  ecqusaddcl  14101  rnglz  14351  qusmulrng  14978  quscrng  14979  dvdsrzring  15047  bcmono  16337  lgsprme0  16399  gausslemma2dlem0e  16410  gausslemma2dlem1a  16415  gausslemma2dlem6  16424  lgsquadlem2  16435  2lgsoddprm  16470  usgrislfuspgrdom  16669  edgssv2en  16678  umgr2edg  16686  uspgredg2v  16700  subupgr  16752  subusgr  16754  vtxdfifiun  16776  eupth2lem3lem3fi  16949