rcp-FR2.SH - bfol.mm Proof Explorer

	bfol.mm Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > PE Home > Th. List > rcp-FR2.SH

Theorem rcp-FR2.SH 42

Description: Inference from rcp-FR2 41.

**Hypothesis**
Ref	Expression
rcp-FR2.SH.1	⊢ (𝛾₂ → (𝛾₁ → (𝜑 → 𝜓)))

**Assertion**
Ref	Expression
rcp-FR2.SH	⊢ ((𝛾₂ → (𝛾₁ → 𝜑)) → (𝛾₂ → (𝛾₁ → 𝜓)))

**Proof of Theorem rcp-FR2.SH**
Step	Hyp	Ref	Expression
1		rcp-FR2.SH.1	. 2 ⊢ (𝛾₂ → (𝛾₁ → (𝜑 → 𝜓)))
2		rcp-FR2 41	. 2 ⊢ ((𝛾₂ → (𝛾₁ → (𝜑 → 𝜓))) → ((𝛾₂ → (𝛾₁ → 𝜑)) → (𝛾₂ → (𝛾₁ → 𝜓))))
3	1, 2	ax-MP 14	1 ⊢ ((𝛾₂ → (𝛾₁ → 𝜑)) → (𝛾₂ → (𝛾₁ → 𝜓)))

Colors of variables: wff objvar term class

Syntax hints: → wff-imp 10

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