Theorem frege7 44651

Description: A closed form of syl6 36. The first antecedent is used to replace the consequent of the second antecedent. Proposition 7 of [Frege1879] p. 34. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
frege7	⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜃 → 𝜑)) → (𝜒 → (𝜃 → 𝜓))))

Proof of Theorem frege7

Step	Hyp	Ref	Expression
1		frege5 44643	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜃 → 𝜑) → (𝜃 → 𝜓)))
2		frege6 44649	. 2 ⊢ (((𝜑 → 𝜓) → ((𝜃 → 𝜑) → (𝜃 → 𝜓))) → ((𝜑 → 𝜓) → ((𝜒 → (𝜃 → 𝜑)) → (𝜒 → (𝜃 → 𝜓)))))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜃 → 𝜑)) → (𝜒 → (𝜃 → 𝜓))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-frege1 44633  ax-frege2 44634

This theorem is used by:  frege32  44678  frege67a  44728  frege67b  44755  frege67c  44773  frege94  44800  frege107  44813  frege113  44819