Theorem 19.20ii 692

Description: Inference quantifying antecedent, nested antecedent, and consequent.

Hypothesis

Ref	Expression
19.20ii.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
19.20ii	⊢ (∀xφ → (∀xψ → ∀xχ))

Proof of Theorem 19.20ii

Step	Hyp	Ref	Expression
1		19.20ii.1	. . 3 ⊢ (φ → (ψ → χ))
2	1	19.20i 691	. 2 ⊢ (∀xφ → ∀x(ψ → χ))
3		19.20 690	. 2 ⊢ (∀x(ψ → χ) → (∀xψ → ∀xχ))
4	2, 3	syl 12	1 ⊢ (∀xφ → (∀xψ → ∀xχ))

Syntax hints:   → wi 2  ∀wal 672

This theorem is referenced by:  19.20d 693  19.15 694  hbnt 710  19.22 722  19.26 749  del34 835  del35 836  del36 838  cbv1 845  hbsb3 875  sbi1 884  sbied 903  hbsb4 905  sb9i 920  sbal1 996  immo 1043  r19.20 1251  ralcom2 1314  sstr2 1510  difin0ss 1753  intss 1983

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

metamath.org