Description: Virtual deduction proof of syl5imp . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
| 1:: | |- (. ( ph -> ( ps -> ch ) ) ->. ( ph -> ( ps -> ch ) ) ). |
| 2:1,?: e1a | |- (. ( ph -> ( ps -> ch ) ) ->. ( ps -> ( ph -> ch ) ) ). |
| 3:: | |- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( th -> ps ) ). |
| 4:3,2,?: e21 | |- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( th -> ( ph -> ch ) ) ). |
| 5:4,?: e2 | |- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( ph -> ( th -> ch ) ) ). |
| 6:5: | |- (. ( ph -> ( ps -> ch ) ) ->. ( ( th -> ps ) -> ( ph -> ( th -> ch ) ) ) ). |
| qed:6: | |- ( ( ph -> ( ps -> ch ) ) -> ( ( th -> ps ) -> ( ph -> ( th -> ch ) ) ) ) |
| Ref | Expression | ||
|---|---|---|---|
| Assertion | syl5impVD | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜃 → 𝜓 ) → ( 𝜑 → ( 𝜃 → 𝜒 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idn2 | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) , ( 𝜃 → 𝜓 ) ▶ ( 𝜃 → 𝜓 ) ) | |
| 2 | idn1 | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ▶ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) | |
| 3 | pm2.04 | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜓 → ( 𝜑 → 𝜒 ) ) ) | |
| 4 | 2 3 | e1a | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ▶ ( 𝜓 → ( 𝜑 → 𝜒 ) ) ) |
| 5 | imim1 | ⊢ ( ( 𝜃 → 𝜓 ) → ( ( 𝜓 → ( 𝜑 → 𝜒 ) ) → ( 𝜃 → ( 𝜑 → 𝜒 ) ) ) ) | |
| 6 | 1 4 5 | e21 | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) , ( 𝜃 → 𝜓 ) ▶ ( 𝜃 → ( 𝜑 → 𝜒 ) ) ) |
| 7 | pm2.04 | ⊢ ( ( 𝜃 → ( 𝜑 → 𝜒 ) ) → ( 𝜑 → ( 𝜃 → 𝜒 ) ) ) | |
| 8 | 6 7 | e2 | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) , ( 𝜃 → 𝜓 ) ▶ ( 𝜑 → ( 𝜃 → 𝜒 ) ) ) |
| 9 | 8 | in2 | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ▶ ( ( 𝜃 → 𝜓 ) → ( 𝜑 → ( 𝜃 → 𝜒 ) ) ) ) |
| 10 | 9 | in1 | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜃 → 𝜓 ) → ( 𝜑 → ( 𝜃 → 𝜒 ) ) ) ) |