Theorem anim1i 338

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 336	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  sylanl1  399  sylanr1  401  mpan10  465  sbcof2  1782  sbidm  1823  disamis  2110  r19.28v  2560  fun11uni  5193  fabexg  5310  fores  5354  f1oabexg  5379  fun11iun  5388  fvelrnb  5469  ssimaex  5482  foeqcnvco  5691  f1eqcocnv  5692  isoini  5719  brtposg  6151  tfrcllemssrecs  6249  fiintim  6817  djuex  6928  elni2  7122  dmaddpqlem  7185  nqpi  7186  ltexnqq  7216  nq0nn  7250  nqnq0a  7262  nqnq0m  7263  elnp1st2nd  7284  mullocprlem  7378  cnegexlem3  7939  divmulasscomap  8456  lediv2a  8653  btwnz  9170  eluz2b2  9397  uz2mulcl  9402  eqreznegel  9406  elioo4g  9717  fz0fzelfz0  9904  fz0fzdiffz0  9907  2ffzeq  9918  elfzodifsumelfzo  9978  elfzom1elp1fzo  9979  zpnn0elfzo  9984  ioo0  10037  zmodidfzoimp  10127  expcl2lemap  10305  mulreap  10636  redivap  10646  imdivap  10653  caucvgrelemcau  10752  negdvdsb  11509  muldvds1  11518  muldvds2  11519  dvdsdivcl  11548  nn0ehalf  11600  nn0oddm1d2  11606  nnoddm1d2  11607  infssuzex  11642  divgcdnn  11663  coprmgcdb  11769  divgcdcoprm0  11782  pw2dvdslemn  11843