Theorem anim1i 269

Description: Introduce conjunct to both sides of an implication.

Hypothesis

Ref	Expression
anim1i.1	⊢ (φ → ψ)

Assertion

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

Proof of Theorem anim1i

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

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  difex2 1951  cores 2659  fun11uni 2707  fores 2794  f1o2 2804  tz6.12-1 2842  tz7.48lem 2993  tz7.49c 2998  ndmoprass 3062  nnaordex 3191  nnawordex 3192  sbthlem9 3357  pssnn 3428  fiint 3445  inf1 3458  ltexpq 3874  prnmadd 3894  genpnnp 3902  prlem934 3933  prlem936 3949  reclem1pr 3950  reclem2pr 3951  suplem1pr 3955  suppsr2 4017  suppsr3 4018  divasst 4239  divnegt 4259  divadddivt 4264  elnn0nn 4593  btwnz 4613  qnegclt 4643  infxpidmlem7 4939  infxpidmlem8 4940  infmap2lem1 4951  hlimcaui 5141  ocsh 5164  chocuni 5179  projlem16 5208  5oalem2 5545  5oalem5 5548  3oalem2 5553  pjjs 5585  stge1 5679  hatomistic 5755  mdsymlem2 5777  mdsymlem5 5780

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org