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  1858  sbidm  1899  disamis  2191  r19.28v  2662  fun11uni  5407  fabexg  5532  fores  5578  f1oabexg  5604  fun11iun  5613  fdmeu  5698  fvelrnb  5702  ssimaex  5716  foeqcnvco  5941  f1eqcocnv  5942  isoini  5969  brtposg  6463  tfrcllemssrecs  6561  fiintim  7166  djuex  7285  elni2  7577  dmaddpqlem  7640  nqpi  7641  ltexnqq  7671  nq0nn  7705  nqnq0a  7717  nqnq0m  7718  elnp1st2nd  7739  mullocprlem  7833  cnegexlem3  8399  divmulasscomap  8919  lediv2a  9118  btwnz  9642  eluz2b2  9880  uz2mulcl  9885  eqreznegel  9891  elioo4g  10212  fz0fzelfz0  10405  fz0fzdiffz0  10408  2ffzeq  10419  elfzodifsumelfzo  10490  elfzom1elp1fzo  10491  zpnn0elfzo  10496  infssuzex  10537  ioo0  10563  zmodidfzoimp  10660  expcl2lemap  10857  iswrdsymb  11178  ccatcl  11217  ccatsymb  11226  swrdfv2  11291  swrdsbslen  11294  swrdspsleq  11295  pfxswrd  11334  pfxccatin12lem3  11360  pfxccatpfx2  11365  swrdccat3blem  11367  reuccatpfxs1  11375  mulreap  11485  redivap  11495  imdivap  11502  caucvgrelemcau  11601  zproddc  12201  fprodseq  12205  p1modz1  12416  negdvdsb  12429  muldvds1  12438  muldvds2  12439  dvdsdivcl  12472  nn0ehalf  12525  nn0oddm1d2  12531  nnoddm1d2  12532  divgcdnn  12607  coprmgcdb  12721  divgcdcoprm0  12734  pw2dvdslemn  12798  oddprmdvds  12988  4sqexercise1  13032  4sqexercise2  13033  grpissubg  13842  ecqusaddd  13886  ecqusaddcl  13887  rnglz  14020  qusmulrng  14608  quscrng  14609  dvdsrzring  14679  lgsprme0  15841  gausslemma2dlem0e  15852  gausslemma2dlem1a  15857  gausslemma2dlem6  15866  lgsquadlem2  15877  2lgsoddprm  15912  usgrislfuspgrdom  16111  edgssv2en  16120  umgr2edg  16128  uspgredg2v  16142  subupgr  16194  subusgr  16196  vtxdfifiun  16218  eupth2lem3lem3fi  16391