Theorem wl-impchain-a1-x

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 , that allows us prepending an arbitrary antecedent to an implication chain. Using our antecedent swapping theorems described in wl-impchain-com-n.m , 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 , a1d and a1dd 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 series developed before. (Contributed by Wolf Lammen, 20-Jun-2020)

	Ref	Expression
Assertion	wl-impchain-a1-x	|- T.

Proof

Step	Hyp	Ref	Expression
1		tru	|- T.