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

Theorem wl-impchain-com-1.x 33586
 Description: It is often convenient to have the antecedent under focus in first position, so we can apply immediate theorem forms (as opposed to deduction, tautology form). This series of theorems swaps the first with the last antecedent in an implication chain. This kind of swapping is self-inverse, whence we prefer it over, say, rotating theorems. A consequent can hide a tail of a longer chain, so theorems of this series appear as swapping a pair of antecedents with fixed offsets. This form of swapping antecedents is flexible enough to allow for any permutation of antecedents in an implication chain. The first elements of this series correspond to com12 32, com13 88, com14 96 and com15 101 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-mp-x 33582 series developed before. (Contributed by Wolf Lammen, 17-Nov-2019.)
Assertion
Ref Expression
wl-impchain-com-1.x

Proof of Theorem wl-impchain-com-1.x
StepHypRef Expression
1 tru 1636 1
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1633 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 197  df-tru 1635 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator