Metamath Proof Explorer

Theorem spthonpthon

Description: A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021)

Ref Expression
Assertion spthonpthon ⊢ F A SPathsOn ⁡ G B P → F A PathsOn ⁡ G B P

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 spthonprop ⊢ F A SPathsOn ⁡ G B P → G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P
3 3simpc ⊢ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
4 3 3anim1i ⊢ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P
5 spthispth ⊢ F SPaths ⁡ G P → F Paths ⁡ G P
6 5 anim2i ⊢ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P → F A TrailsOn ⁡ G B P ∧ F Paths ⁡ G P
7 6 3ad2ant3 ⊢ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P → F A TrailsOn ⁡ G B P ∧ F Paths ⁡ G P
8 1 ispthson ⊢ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V → F A PathsOn ⁡ G B P ↔ F A TrailsOn ⁡ G B P ∧ F Paths ⁡ G P
9 8 3adant3 ⊢ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P → F A PathsOn ⁡ G B P ↔ F A TrailsOn ⁡ G B P ∧ F Paths ⁡ G P
10 7 9 mpbird ⊢ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P → F A PathsOn ⁡ G B P
11 2 4 10 3syl ⊢ F A SPathsOn ⁡ G B P → F A PathsOn ⁡ G B P