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  1856  sbidm  1897  disamis  2189  r19.28v  2659  fun11uni  5387  fabexg  5509  fores  5554  f1oabexg  5580  fun11iun  5589  fdmeu  5670  fvelrnb  5674  ssimaex  5688  foeqcnvco  5907  f1eqcocnv  5908  isoini  5935  brtposg  6390  tfrcllemssrecs  6488  fiintim  7081  djuex  7198  elni2  7489  dmaddpqlem  7552  nqpi  7553  ltexnqq  7583  nq0nn  7617  nqnq0a  7629  nqnq0m  7630  elnp1st2nd  7651  mullocprlem  7745  cnegexlem3  8311  divmulasscomap  8831  lediv2a  9030  btwnz  9554  eluz2b2  9786  uz2mulcl  9791  eqreznegel  9797  elioo4g  10118  fz0fzelfz0  10311  fz0fzdiffz0  10314  2ffzeq  10325  elfzodifsumelfzo  10394  elfzom1elp1fzo  10395  zpnn0elfzo  10400  infssuzex  10440  ioo0  10466  zmodidfzoimp  10563  expcl2lemap  10760  iswrdsymb  11076  ccatcl  11114  ccatsymb  11123  swrdfv2  11181  swrdsbslen  11184  swrdspsleq  11185  pfxswrd  11224  pfxccatin12lem3  11250  pfxccatpfx2  11255  swrdccat3blem  11257  reuccatpfxs1  11265  mulreap  11361  redivap  11371  imdivap  11378  caucvgrelemcau  11477  zproddc  12076  fprodseq  12080  p1modz1  12291  negdvdsb  12304  muldvds1  12313  muldvds2  12314  dvdsdivcl  12347  nn0ehalf  12400  nn0oddm1d2  12406  nnoddm1d2  12407  divgcdnn  12482  coprmgcdb  12596  divgcdcoprm0  12609  pw2dvdslemn  12673  oddprmdvds  12863  4sqexercise1  12907  4sqexercise2  12908  grpissubg  13717  ecqusaddd  13761  ecqusaddcl  13762  rnglz  13894  qusmulrng  14481  quscrng  14482  dvdsrzring  14552  lgsprme0  15706  gausslemma2dlem0e  15717  gausslemma2dlem1a  15722  gausslemma2dlem6  15731  lgsquadlem2  15742  2lgsoddprm  15777  usgrislfuspgrdom  15973  edgssv2en  15982  umgr2edg  15990  uspgredg2v  16004