 Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  syl5impVD Structured version   Visualization version   GIF version

Theorem syl5impVD 38121
Description: Virtual deduction proof of syl5imp 37739. 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:: ⊢ (   (𝜑 → (𝜓 → 𝜒))   ▶   (𝜑 → (𝜓 → 𝜒))   ) 2:1,?: e1a 37873 ⊢ (   (𝜑 → (𝜓 → 𝜒))   ▶   (𝜓 → (𝜑 → 𝜒))   ) 3:: ⊢ (   (𝜑 → (𝜓 → 𝜒))   ,   (𝜃 → 𝜓)   ▶   (𝜃 → 𝜓)   ) 4:3,2,?: e21 37978 ⊢ (   (𝜑 → (𝜓 → 𝜒))   ,   (𝜃 → 𝜓)   ▶   (𝜃 → (𝜑 → 𝜒))   ) 5:4,?: e2 37877 ⊢ (   (𝜑 → (𝜓 → 𝜒))   ,   (𝜃 → 𝜓)   ▶   (𝜑 → (𝜃 → 𝜒))   ) 6:5: ⊢ (   (𝜑 → (𝜓 → 𝜒))   ▶   ((𝜃 → 𝜓) → (𝜑 → (𝜃 → 𝜒)))   ) qed:6: ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜓) → (𝜑 → (𝜃 → 𝜒))))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
syl5impVD ((𝜑 → (𝜓𝜒)) → ((𝜃𝜓) → (𝜑 → (𝜃𝜒))))

Proof of Theorem syl5impVD
StepHypRef Expression
1 idn2 37859 . . . . 5 (   (𝜑 → (𝜓𝜒))   ,   (𝜃𝜓)   ▶   (𝜃𝜓)   )
2 idn1 37811 . . . . . 6 (   (𝜑 → (𝜓𝜒))   ▶   (𝜑 → (𝜓𝜒))   )
3 pm2.04 88 . . . . . 6 ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
42, 3e1a 37873 . . . . 5 (   (𝜑 → (𝜓𝜒))   ▶   (𝜓 → (𝜑𝜒))   )
5 imim1 81 . . . . 5 ((𝜃𝜓) → ((𝜓 → (𝜑𝜒)) → (𝜃 → (𝜑𝜒))))
61, 4, 5e21 37978 . . . 4 (   (𝜑 → (𝜓𝜒))   ,   (𝜃𝜓)   ▶   (𝜃 → (𝜑𝜒))   )
7 pm2.04 88 . . . 4 ((𝜃 → (𝜑𝜒)) → (𝜑 → (𝜃𝜒)))
86, 7e2 37877 . . 3 (   (𝜑 → (𝜓𝜒))   ,   (𝜃𝜓)   ▶   (𝜑 → (𝜃𝜒))   )
98in2 37851 . 2 (   (𝜑 → (𝜓𝜒))   ▶   ((𝜃𝜓) → (𝜑 → (𝜃𝜒)))   )
109in1 37808 1 ((𝜑 → (𝜓𝜒)) → ((𝜃𝜓) → (𝜑 → (𝜃𝜒))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 196  df-an 385  df-vd1 37807  df-vd2 37815 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator