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  8467  divmulasscomap  8990  lediv2a  9189  btwnz  9718  eluz2b2  9956  uz2mulcl  9961  eqreznegel  9967  elioo4g  10289  fz0fzelfz0  10486  fz0fzdiffz0  10489  2ffzeq  10500  elfzodifsumelfzo  10571  elfzom1elp1fzo  10572  zpnn0elfzo  10577  infssuzex  10618  ioo0  10646  zmodidfzoimp  10743  expcl2lemap  10940  hashfibclem  11234  iswrdsymb  11270  ccatcl  11309  ccatsymb  11318  swrdfv2  11383  swrdsbslen  11386  swrdspsleq  11387  pfxswrd  11426  pfxccatin12lem3  11452  pfxccatpfx2  11457  swrdccat3blem  11459  reuccatpfxs1  11467  mulreap  11577  redivap  11587  imdivap  11594  caucvgrelemcau  11694  zproddc  12294  fprodseq  12298  p1modz1  12509  negdvdsb  12522  muldvds1  12531  muldvds2  12532  dvdsdivcl  12565  nn0ehalf  12618  nn0oddm1d2  12624  nnoddm1d2  12625  divgcdnn  12700  coprmgcdb  12814  divgcdcoprm0  12827  pw2dvdslemn  12891  oddprmdvds  13081  4sqexercise1  13125  4sqexercise2  13126  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemth  13229  grpissubg  13951  ecqusaddd  13995  ecqusaddcl  13996  rnglz  14188  qusmulrng  14810  quscrng  14811  dvdsrzring  14881  lgsprme0  16045  gausslemma2dlem0e  16056  gausslemma2dlem1a  16061  gausslemma2dlem6  16070  lgsquadlem2  16081  2lgsoddprm  16116  usgrislfuspgrdom  16315  edgssv2en  16324  umgr2edg  16332  uspgredg2v  16346  subupgr  16398  subusgr  16400  vtxdfifiun  16422  eupth2lem3lem3fi  16595