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  2192  r19.28v  2671  fun11uni  5425  fabexg  5553  fores  5599  f1oabexg  5625  fun11iun  5634  fdmeu  5719  fvelrnb  5723  ssimaex  5737  foeqcnvco  5962  f1eqcocnv  5963  isoini  5990  brtposg  6484  tfrcllemssrecs  6582  fiintim  7190  djuex  7333  elni2  7628  dmaddpqlem  7691  nqpi  7692  ltexnqq  7722  nq0nn  7756  nqnq0a  7768  nqnq0m  7769  elnp1st2nd  7790  mullocprlem  7884  cnegexlem3  8449  divmulasscomap  8969  lediv2a  9168  btwnz  9696  eluz2b2  9934  uz2mulcl  9939  eqreznegel  9945  elioo4g  10266  fz0fzelfz0  10460  fz0fzdiffz0  10463  2ffzeq  10474  elfzodifsumelfzo  10545  elfzom1elp1fzo  10546  zpnn0elfzo  10551  infssuzex  10592  ioo0  10618  zmodidfzoimp  10715  expcl2lemap  10912  hashfibclem  11202  iswrdsymb  11238  ccatcl  11277  ccatsymb  11286  swrdfv2  11351  swrdsbslen  11354  swrdspsleq  11355  pfxswrd  11394  pfxccatin12lem3  11420  pfxccatpfx2  11425  swrdccat3blem  11427  reuccatpfxs1  11435  mulreap  11545  redivap  11555  imdivap  11562  caucvgrelemcau  11661  zproddc  12261  fprodseq  12265  p1modz1  12476  negdvdsb  12489  muldvds1  12498  muldvds2  12499  dvdsdivcl  12532  nn0ehalf  12585  nn0oddm1d2  12591  nnoddm1d2  12592  divgcdnn  12667  coprmgcdb  12781  divgcdcoprm0  12794  pw2dvdslemn  12858  oddprmdvds  13048  4sqexercise1  13092  4sqexercise2  13093  grpissubg  13903  ecqusaddd  13947  ecqusaddcl  13948  rnglz  14081  qusmulrng  14672  quscrng  14673  dvdsrzring  14743  lgsprme0  15907  gausslemma2dlem0e  15918  gausslemma2dlem1a  15923  gausslemma2dlem6  15932  lgsquadlem2  15943  2lgsoddprm  15978  usgrislfuspgrdom  16177  edgssv2en  16186  umgr2edg  16194  uspgredg2v  16208  subupgr  16260  subusgr  16262  vtxdfifiun  16284  eupth2lem3lem3fi  16457