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 32458
 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-a1i 32427, that allows us prepending an arbitrary antecedent to an implication chain. Using our antecedent swapping theorems described in wl-impchain-com-n.m 32454, 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 48 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 32449 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 1479 1
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1476 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-tru 1478 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator