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  6424  nqnq0a  6436  nqnq0m  6437  elnp1st2nd  6458  mullocprlem  6550  cnegexlem3  6965  lediv2a  7622  btwnz  8113  eluz2b2  8296  uz2mulcl  8301  eqreznegel  8305  elioo4g  8553  fz0fzelfz0  8734  fz0fzdiffz0  8737  2ffzeq  8748  elfzodifsumelfzo  8807  elfzom1elp1fzo  8808  zpnn0elfzo  8813  expcl2lemap  8901  mulreap  9072  redivap  9082  imdivap  9089