Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-prv2 Structured version   Visualization version   GIF version

Axiom ax-prv2 33830
Description: Second property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
Assertion
Ref Expression
ax-prv2 (Prv (𝜑𝜓) → (Prv 𝜑 → Prv 𝜓))

Detailed syntax breakdown of Axiom ax-prv2
StepHypRef Expression
1 wph . . . 4 wff 𝜑
2 wps . . . 4 wff 𝜓
31, 2wi 4 . . 3 wff (𝜑𝜓)
43cprvb 33828 . 2 wff Prv (𝜑𝜓)
51cprvb 33828 . . 3 wff Prv 𝜑
62cprvb 33828 . . 3 wff Prv 𝜓
75, 6wi 4 . 2 wff (Prv 𝜑 → Prv 𝜓)
84, 7wi 4 1 wff (Prv (𝜑𝜓) → (Prv 𝜑 → Prv 𝜓))
Colors of variables: wff setvar class
This axiom is referenced by:  prvlem1  33832  prvlem2  33833
  Copyright terms: Public domain W3C validator