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

Theorem wl-impchain-com-n.m 34619
Description: This series of theorems allow swapping any two antecedents in an implication chain. The theorem names follow a pattern wl-impchain-com-n.m with integral numbers n < m, that swaps the m-th antecedent with n-th one in an implication chain. It is sufficient to restrict the length of the chain to m, too, since the consequent can be assumed to be the tail right of the m-th antecedent of any arbitrary sized implication chain. We further assume n > 1, since the wl-impchain-com-1.x 34614 series already covers the special case n = 1.

Being able to swap any two antecedents in an implication chain lays the foundation of permuting its antecedents arbitrarily.

The proofs of this series aim at automated proofing using a simple scheme. Any instance of this series is a triple step of swapping the first and n-th antecedent, then the first and the m-th, then the first and the n-th antecedent again. Each of these steps is an instance of the wl-impchain-com-1.x 34614 series. (Contributed by Wolf Lammen, 17-Nov-2019.)

Assertion
Ref Expression
wl-impchain-com-n.m

Proof of Theorem wl-impchain-com-n.m
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