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  382  sylanr1  384  mpan10  443  sbcof2  1688  sbidm  1728  disamis  2008  fun11uni  4912  fabexg  5020  fores  5058  f1oabexg  5081  fun11iun  5090  fvelrnb  5164  ssimaex  5177  foeqcnvco  5373  f1eqcocnv  5374  isoini  5400  brtposg  5810  elni2  6298  dmaddpqlem  6361  nqpi  6362  ltexnqq  6391  nq0nn  6425  nqnq0a  6437  nqnq0m  6438  elnp1st2nd  6459  mullocprlem  6551  cnegexlem3  6985  lediv2a  7642  btwnz  8133  eluz2b2  8316  uz2mulcl  8321  eqreznegel  8325  elioo4g  8573  fz0fzelfz0  8754  fz0fzdiffz0  8757  2ffzeq  8768  elfzodifsumelfzo  8827  elfzom1elp1fzo  8828  zpnn0elfzo  8833  expcl2lemap  8921  mulreap  9092  redivap  9102  imdivap  9109