Metamath Proof Explorer


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 φ