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  2753  rspc2ev  2964  reu3  3027  difrab  3530  sfinltfin  4536  vfinspnn  4542  vinf  4556  fof  5270  fv3  5342  fvelimab  5371  fvopab4t  5386  dff2  5420  dffo5  5425  dff1o6  5476  oprabid  5551  ssoprab2i  5581  ndmovass  5619  ndmovdistr  5620  oqelins4  5795