Theorem 19.20ii 993

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 990	. 2 ⊢ (∀xφ → ∀x(ψ → χ))
3		19.20 992	. 2 ⊢ (∀x(ψ → χ) → (∀xψ → ∀xχ))
4	2, 3	syl 10	1 ⊢ (∀xφ → (∀xψ → ∀xχ))

Syntax hints:   → wi 3  ∀wal 952

This theorem is referenced by:  19.20d 994  19.15 995  hbnt 1000  19.22 1037  19.26 1065  ax10o 1137  a4imt 1156  cbv1 1160  sbied 1193  sbi1 1230  hbsb4 1246  sb9i 1261  sbal1 1344  immo 1415  2mo 1445  r19.20 1699  ralcom2 1773  sstr2 2067  difin0ss 2328  intss 2549

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

Copyright terms: Public domain