Theorem anim1i 333

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  sylanl1  394  sylanr1  396  mpan10  457  sbcof2  1731  sbidm  1772  disamis  2052  fun11uni  4989  fabexg  5097  fores  5135  f1oabexg  5158  fun11iun  5167  fvelrnb  5242  ssimaex  5255  foeqcnvco  5450  f1eqcocnv  5451  isoini  5477  brtposg  5892  elni2  6504  dmaddpqlem  6567  nqpi  6568  ltexnqq  6598  nq0nn  6632  nqnq0a  6644  nqnq0m  6645  elnp1st2nd  6666  mullocprlem  6760  cnegexlem3  7285  divmulasscomap  7784  lediv2a  7973  btwnz  8466  eluz2b2  8690  uz2mulcl  8695  eqreznegel  8699  elioo4g  8957  fz0fzelfz0  9138  fz0fzdiffz0  9141  2ffzeq  9151  elfzodifsumelfzo  9210  elfzom1elp1fzo  9211  zpnn0elfzo  9216  ioo0  9268  zmodidfzoimp  9356  expcl2lemap  9488  mulreap  9751  redivap  9761  imdivap  9768  caucvgrelemcau  9866  negdvdsb  10211  muldvds1  10220  muldvds2  10221  dvdsdivcl  10250  nn0ehalf  10303  nn0oddm1d2  10309  nnoddm1d2  10310  infssuzex  10345  divgcdnn  10366  coprmgcdb  10470  divgcdcoprm0  10483  pw2dvdslemn  10543