Theorem anim12d 546

Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)

Hypotheses

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

Assertion

Ref	Expression
anim12d	⊢ (φ → ((ψ ∧ θ) → (χ ∧ τ)))

Proof of Theorem anim12d

Step	Hyp	Ref	Expression
1		anim12d.1	. 2 ⊢ (φ → (ψ → χ))
2		anim12d.2	. 2 ⊢ (φ → (θ → τ))
3		idd 21	. 2 ⊢ (φ → ((χ ∧ τ) → (χ ∧ τ)))
4	1, 2, 3	syl2and 469	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:  anim1d  547  anim2d  548  prth  554  im2anan9  808  anim12dan  810  3anim123d  1259  2euswap  2280  ssunsn2  3865  leltfintr  4458  ltfintr  4459  xp11  5056  2elresin  5194  fun  5236  dff13  5471  isotr  5495  enmap2lem4  6066  enmap1lem4  6072  nnltp1c  6262  nchoicelem17  6305  fnfrec  6320