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  5394  fabexg  5518  fores  5563  f1oabexg  5589  fun11iun  5598  fdmeu  5682  fvelrnb  5686  ssimaex  5700  foeqcnvco  5923  f1eqcocnv  5924  isoini  5951  brtposg  6411  tfrcllemssrecs  6509  fiintim  7109  djuex  7226  elni2  7517  dmaddpqlem  7580  nqpi  7581  ltexnqq  7611  nq0nn  7645  nqnq0a  7657  nqnq0m  7658  elnp1st2nd  7679  mullocprlem  7773  cnegexlem3  8339  divmulasscomap  8859  lediv2a  9058  btwnz  9582  eluz2b2  9815  uz2mulcl  9820  eqreznegel  9826  elioo4g  10147  fz0fzelfz0  10340  fz0fzdiffz0  10343  2ffzeq  10354  elfzodifsumelfzo  10424  elfzom1elp1fzo  10425  zpnn0elfzo  10430  infssuzex  10470  ioo0  10496  zmodidfzoimp  10593  expcl2lemap  10790  iswrdsymb  11107  ccatcl  11146  ccatsymb  11155  swrdfv2  11216  swrdsbslen  11219  swrdspsleq  11220  pfxswrd  11259  pfxccatin12lem3  11285  pfxccatpfx2  11290  swrdccat3blem  11292  reuccatpfxs1  11300  mulreap  11396  redivap  11406  imdivap  11413  caucvgrelemcau  11512  zproddc  12111  fprodseq  12115  p1modz1  12326  negdvdsb  12339  muldvds1  12348  muldvds2  12349  dvdsdivcl  12382  nn0ehalf  12435  nn0oddm1d2  12441  nnoddm1d2  12442  divgcdnn  12517  coprmgcdb  12631  divgcdcoprm0  12644  pw2dvdslemn  12708  oddprmdvds  12898  4sqexercise1  12942  4sqexercise2  12943  grpissubg  13752  ecqusaddd  13796  ecqusaddcl  13797  rnglz  13929  qusmulrng  14517  quscrng  14518  dvdsrzring  14588  lgsprme0  15742  gausslemma2dlem0e  15753  gausslemma2dlem1a  15758  gausslemma2dlem6  15767  lgsquadlem2  15778  2lgsoddprm  15813  usgrislfuspgrdom  16009  edgssv2en  16018  umgr2edg  16026  uspgredg2v  16040  vtxdfifiun  16083