Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-impchain-mp-0 Structured version   Visualization version   GIF version

Theorem wl-impchain-mp-0 33609
Description: This theorem is the start of a proof recursion scheme where we replace the consequent of an implication chain. The number '0' in the theorem name indicates that the modified chain has no antecedents.

This theorem is in fact a copy of ax-mp 5, and is repeated here to emphasize the recursion using similar theorem names. (Contributed by Wolf Lammen, 6-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
wl-impchain-mp-0.a 𝜓
wl-impchain-mp-0.b (𝜓𝜑)
Ref Expression
wl-impchain-mp-0 𝜑

Proof of Theorem wl-impchain-mp-0
StepHypRef Expression
1 wl-impchain-mp-0.a . 2 𝜓
2 wl-impchain-mp-0.b . 2 (𝜓𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5
This theorem is referenced by:  wl-impchain-mp-1  33610  wl-impchain-com-1.2  33614
  Copyright terms: Public domain W3C validator