Theorem anim1i 323

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 321	1 ⊢ ((φ ∧ χ) → (ψ ∧ χ))

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  sylanl1  384  sylanr1  386  mpan10  446  sbcof2  1669  sbidm  1709  disamis  1989  fun11uni  4891  fabexg  4998  fores  5036  f1oabexg  5059  fun11iun  5068  fvelrnb  5142  ssimaex  5155  foeqcnvco  5351  f1eqcocnv  5352  isoini  5378  brtposg  5787  elni2  6168  dmaddpqlem  6230  nqpi  6231  ltexnqq  6260  nq0nn  6291  nqnq0a  6303  nqnq0m  6304  elnp1st2nd  6324  mullocprlem  6408  cnegexlem3  6775