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  1824  sbidm  1865  disamis  2156  r19.28v  2625  fun11uni  5329  fabexg  5448  fores  5493  f1oabexg  5519  fun11iun  5528  fvelrnb  5611  ssimaex  5625  foeqcnvco  5840  f1eqcocnv  5841  isoini  5868  brtposg  6321  tfrcllemssrecs  6419  fiintim  7001  djuex  7118  elni2  7400  dmaddpqlem  7463  nqpi  7464  ltexnqq  7494  nq0nn  7528  nqnq0a  7540  nqnq0m  7541  elnp1st2nd  7562  mullocprlem  7656  cnegexlem3  8222  divmulasscomap  8742  lediv2a  8941  btwnz  9464  eluz2b2  9696  uz2mulcl  9701  eqreznegel  9707  elioo4g  10028  fz0fzelfz0  10221  fz0fzdiffz0  10224  2ffzeq  10235  elfzodifsumelfzo  10296  elfzom1elp1fzo  10297  zpnn0elfzo  10302  infssuzex  10342  ioo0  10368  zmodidfzoimp  10465  expcl2lemap  10662  iswrdsymb  10972  mulreap  11048  redivap  11058  imdivap  11065  caucvgrelemcau  11164  zproddc  11763  fprodseq  11767  p1modz1  11978  negdvdsb  11991  muldvds1  12000  muldvds2  12001  dvdsdivcl  12034  nn0ehalf  12087  nn0oddm1d2  12093  nnoddm1d2  12094  divgcdnn  12169  coprmgcdb  12283  divgcdcoprm0  12296  pw2dvdslemn  12360  oddprmdvds  12550  4sqexercise1  12594  4sqexercise2  12595  grpissubg  13402  ecqusaddd  13446  ecqusaddcl  13447  rnglz  13579  qusmulrng  14166  quscrng  14167  dvdsrzring  14237  lgsprme0  15391  gausslemma2dlem0e  15402  gausslemma2dlem1a  15407  gausslemma2dlem6  15416  lgsquadlem2  15427  2lgsoddprm  15462