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  5397  fabexg  5521  fores  5566  f1oabexg  5592  fun11iun  5601  fdmeu  5685  fvelrnb  5689  ssimaex  5703  foeqcnvco  5926  f1eqcocnv  5927  isoini  5954  brtposg  6415  tfrcllemssrecs  6513  fiintim  7118  djuex  7236  elni2  7527  dmaddpqlem  7590  nqpi  7591  ltexnqq  7621  nq0nn  7655  nqnq0a  7667  nqnq0m  7668  elnp1st2nd  7689  mullocprlem  7783  cnegexlem3  8349  divmulasscomap  8869  lediv2a  9068  btwnz  9592  eluz2b2  9830  uz2mulcl  9835  eqreznegel  9841  elioo4g  10162  fz0fzelfz0  10355  fz0fzdiffz0  10358  2ffzeq  10369  elfzodifsumelfzo  10439  elfzom1elp1fzo  10440  zpnn0elfzo  10445  infssuzex  10486  ioo0  10512  zmodidfzoimp  10609  expcl2lemap  10806  iswrdsymb  11124  ccatcl  11163  ccatsymb  11172  swrdfv2  11237  swrdsbslen  11240  swrdspsleq  11241  pfxswrd  11280  pfxccatin12lem3  11306  pfxccatpfx2  11311  swrdccat3blem  11313  reuccatpfxs1  11321  mulreap  11418  redivap  11428  imdivap  11435  caucvgrelemcau  11534  zproddc  12133  fprodseq  12137  p1modz1  12348  negdvdsb  12361  muldvds1  12370  muldvds2  12371  dvdsdivcl  12404  nn0ehalf  12457  nn0oddm1d2  12463  nnoddm1d2  12464  divgcdnn  12539  coprmgcdb  12653  divgcdcoprm0  12666  pw2dvdslemn  12730  oddprmdvds  12920  4sqexercise1  12964  4sqexercise2  12965  grpissubg  13774  ecqusaddd  13818  ecqusaddcl  13819  rnglz  13951  qusmulrng  14539  quscrng  14540  dvdsrzring  14610  lgsprme0  15764  gausslemma2dlem0e  15775  gausslemma2dlem1a  15780  gausslemma2dlem6  15789  lgsquadlem2  15800  2lgsoddprm  15835  usgrislfuspgrdom  16034  edgssv2en  16043  umgr2edg  16051  uspgredg2v  16065  vtxdfifiun  16108