Theorem rcp-FR3.SH 44

Description: Inference from rcp-FR3 43.

Hypothesis

Ref	Expression
rcp-FR3.SH.1	⊢ (𝛾₃ → (𝛾₂ → (𝛾₁ → (𝜑 → 𝜓))))

Assertion

Ref	Expression
rcp-FR3.SH	⊢ ((𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜑))) → (𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜓))))

Proof of Theorem rcp-FR3.SH

Step	Hyp	Ref	Expression
1		rcp-FR3.SH.1	. 2 ⊢ (𝛾₃ → (𝛾₂ → (𝛾₁ → (𝜑 → 𝜓))))
2		rcp-FR3 43	. 2 ⊢ ((𝛾₃ → (𝛾₂ → (𝛾₁ → (𝜑 → 𝜓)))) → ((𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜑))) → (𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜓)))))
3	1, 2	ax-MP 14	1 ⊢ ((𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜑))) → (𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜓))))

Syntax hints:   → wff-imp 10

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-MP 14

This theorem is referenced by:  mpt-P1.8.3AC.2SH  60