Theorem anim2i 552

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
anim1i.1	⊢ (φ → ψ)

Assertion

Ref	Expression
anim2i	⊢ ((χ ∧ φ) → (χ ∧ ψ))

Proof of Theorem anim2i

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (χ → χ)
2		anim1i.1	. 2 ⊢ (φ → ψ)
3	1, 2	anim12i 549	1 ⊢ ((χ ∧ φ) → (χ ∧ ψ))

Syntax hints:   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  sylanl2  632  sylanr2  634  andi  837  sbimi  1652  19.41  1879  ax12olem2  1928  exdistrf  1971  equs45f  1989  eupickb  2269  2eu1  2284  darii  2303  festino  2309  baroco  2310  r19.27av  2752  rspc2ev  2963  reu3  3026  difrab  3529  sfinltfin  4535  vfinspnn  4541  vinf  4555  fof  5269  fv3  5341  fvelimab  5370  fvopab4t  5385  dff2  5419  dffo5  5424  dff1o6  5475  oprabid  5550  ssoprab2i  5580  ndmovass  5618  ndmovdistr  5619  oqelins4  5794