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  7384  elni2  7682  dmaddpqlem  7745  nqpi  7746  ltexnqq  7776  nq0nn  7810  nqnq0a  7822  nqnq0m  7823  elnp1st2nd  7844  mullocprlem  7938  cnegexlem3  8505  divmulasscomap  9029  lediv2a  9228  btwnz  9770  eluz2b2  10013  uz2mulcl  10018  eqreznegel  10024  elioo4g  10347  fz0fzelfz0  10545  fz0fzdiffz0  10548  2ffzeq  10559  elfzodifsumelfzo  10630  elfzom1elp1fzo  10631  zpnn0elfzo  10636  infssuzex  10677  ioo0  10705  zmodidfzoimp  10805  expcl2lemap  11002  hashfibclem  11297  iswrdsymb  11337  ccatcl  11376  ccatsymb  11385  swrdfv2  11450  swrdsbslen  11453  swrdspsleq  11454  pfxswrd  11493  pfxccatin12lem3  11519  pfxccatpfx2  11524  swrdccat3blem  11526  reuccatpfxs1  11534  mulreap  11644  redivap  11654  imdivap  11661  caucvgrelemcau  11761  zproddc  12364  fprodseq  12368  p1modz1  12579  negdvdsb  12592  muldvds1  12601  muldvds2  12602  dvdsdivcl  12635  nn0ehalf  12688  nn0oddm1d2  12694  nnoddm1d2  12695  divgcdnn  12770  coprmgcdb  12884  divgcdcoprm0  12897  pwbdvdslemn  12962  oddprmdvds  13155  4sqexercise1  13199  4sqexercise2  13200  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemth  13332  grpissubg  14048  ecqusaddd  14092  ecqusaddcl  14093  rnglz  14295  qusmulrng  14920  quscrng  14921  dvdsrzring  14989  bcmono  16226  lgsprme0  16283  gausslemma2dlem0e  16294  gausslemma2dlem1a  16299  gausslemma2dlem6  16308  lgsquadlem2  16319  2lgsoddprm  16354  usgrislfuspgrdom  16553  edgssv2en  16562  umgr2edg  16570  uspgredg2v  16584  subupgr  16636  subusgr  16638  vtxdfifiun  16660  eupth2lem3lem3fi  16833