This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes) Axiom scheme ax-4 (Quantified Implication) alsyl
Description: Universally quantified and uncurried (imported) form of syllogism.
Theorem *10.3 in WhiteheadRussell p. 150. (Contributed by Andrew
Salmon , 8-Jun-2011)
Ref
Expression
Assertion
alsyl ⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ( 𝜓 → 𝜒 ) ) → ∀ 𝑥 ( 𝜑 → 𝜒 ) )
Proof
Step
Hyp
Ref
Expression
1
pm3.33 ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) )
2
1
alanimi ⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ( 𝜓 → 𝜒 ) ) → ∀ 𝑥 ( 𝜑 → 𝜒 ) )