rcp-FR1.SH - bfol.mm Proof Explorer

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

Theorem rcp-FR1.SH 40

Description: Inference from rcp-FR1 39.

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

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

**Proof of Theorem rcp-FR1.SH**
Step	Hyp	Ref	Expression
1		rcp-FR1.SH.1	. 2 ⊢ (𝛾₁ → (𝜑 → 𝜓))
2		rcp-FR1 39	. 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-L2 12 ax-MP 14