Theorem wl-section-impchain

Description: An implication like ( ps -> ph ) with one antecedent can easily be extended by prepending more and more antecedents, as in ( ch -> ( ps -> ph ) ) or ( th -> ( ch -> ( ps -> ph ) ) ) . I call these expressions implication chains, and the number of antecedents (number of nodes minus one) denotes their length. A given length often marks just a required minimum value, since the consequent ph itself may represent an implication, or even an implication chain, such hiding part of the whole chain. As an extension, it is useful to consider a single variable ph as a degenerate implication chain of length zero.

Implication chains play a particular role in logic, as all propositional expressions turn out to be convertible to one or more implication chains, their nodes as simple as a variable, or its negation.

So there is good reason to focus on implication chains as a sort of normalized expressions, and build some general theorems around them, with proofs using recursive patterns. This allows for theorems referring to longer and longer implication chains in an automated way.

The theorem names in this section contain the text fragment 'impchain' to point out their relevance to implication chains, followed by a number indicating the (minimal) length of the longest chain involved. (Contributed by Wolf Lammen, 6-Jul-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	wl-section-impchain.hyp	⊢ 𝜑
Assertion	wl-section-impchain	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		wl-section-impchain.hyp	⊢ 𝜑