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

Theorem wl-impchain-a1-x 34623
Description: If an implication chain is assumed (hypothesis) or proven (theorem) to hold, then we may add any extra antecedent to it, without changing its truth. This is expressed in its simplest form in wl-luk-a1i 34592, that allows us prepending an arbitrary antecedent to an implication chain. Using our antecedent swapping theorems described in wl-impchain-com-n.m 34619, we may then move such a prepended antecedent to any desired location within all antecedents. The first series of theorems of this kind adds a single antecedent somewhere to an implication chain. The appended number in the theorem name indicates its position within all antecedents, 1 denoting the head position. A second theorem series extends this idea to multiple additions (TODO).

Adding antecedents to an implication chain usually weakens their universality. The consequent afterwards dependends on more conditions than before, which renders the implication chain less versatile. So you find this proof technique mostly when you adjust a chain to a hypothesis of a rule. A common case are syllogisms merging two implication chains into one.

The first elements of the first series correspond to a1i 11, a1d 25 and a1dd 50 in the main part.

The proofs of this series aim at automated proving using a simple recursive scheme. It employs the previous theorem in the series along with a sample from the wl-impchain-com-1.x 34614 series developed before. (Contributed by Wolf Lammen, 20-Jun-2020.)

Assertion
Ref Expression
wl-impchain-a1-x

Proof of Theorem wl-impchain-a1-x
StepHypRef Expression
1 tru 1532 1
Colors of variables: wff setvar class
Syntax hints:  wtru 1529
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 208  df-tru 1531
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator