Theorem anim12i 549

Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)

Hypotheses

Ref	Expression
anim12i.1	⊢ (φ → ψ)
anim12i.2	⊢ (χ → θ)

Assertion

Ref	Expression
anim12i	⊢ ((φ ∧ χ) → (ψ ∧ θ))

Proof of Theorem anim12i

Step	Hyp	Ref	Expression
1		anim12i.1	. 2 ⊢ (φ → ψ)
2		anim12i.2	. 2 ⊢ (χ → θ)
3		id 19	. 2 ⊢ ((ψ ∧ θ) → (ψ ∧ θ))
4	1, 2, 3	syl2an 463	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:  anim12ci  550  anim1i  551  anim2i  552  sbimi  1652  2mo  2282  cgsex2g  2892  cgsex4g  2893  spc2egv  2942  sseq2  3294  uneqin  3507  undif3  3516  ssunieq  3925  iuneq1  3983  iuneq2  3986  tfin11  4494  sfinltfin  4536  copsex2t  4609  vtoclr  4817  coeq1  4875  coeq2  4876  brco  4884  cnveq  4887  dmeq  4908  dfco2a  5082  funeq  5128  funun  5147  2elresin  5195  funssxp  5234  fssres  5239  f1co  5265  f1ores  5301  resdif  5307  f1oco  5309  fvun  5379  fvreseq  5399  brswap  5510  fununiq  5518  ndmovdistr  5620  ndmovord  5621  trtxp  5782  fntxp  5805  qrpprod  5837  fnpprod  5844  f1opprod  5845  enprmaplem3  6079  peano4nc  6151  cecl  6187