Theorem al2imi 1561

Description: Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
al2imi.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
al2imi	⊢ (∀xφ → (∀xψ → ∀xχ))

Proof of Theorem al2imi

Step	Hyp	Ref	Expression
1		al2imi.1	. . 3 ⊢ (φ → (ψ → χ))
2	1	alimi 1559	. 2 ⊢ (∀xφ → ∀x(ψ → χ))
3		alim 1558	. 2 ⊢ (∀x(ψ → χ) → (∀xψ → ∀xχ))
4	2, 3	syl 15	1 ⊢ (∀xφ → (∀xψ → ∀xχ))

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1546  ax-5 1557

This theorem is referenced by:  alanimi  1562  alimdh  1563  albi  1564  exim  1575  19.33b  1608  sp  1747  spOLD  1748  hbnt  1775  nfndOLD  1792  hbimdOLD  1816  equsalhwOLD  1839  nfaldOLD  1853  dvelimv  1939  ax10lem6  1943  ax9o  1950  ax10o  1952  cbv1h  1978  sbi1  2063  sbal1  2126  ax10o-o  2203  moim  2250  ralim  2686  ceqsalt  2882  difin0ss  3617  intss  3948