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

Theorem wl-impchain-com-3.2.1 33599
Description: This theorem is in fact a copy of com3r 87. The proof is an example of how to arrive at arbitrary permutations of antecedents, using only swapping theorems. The recursion principle is to first swap the correct antecedent to the position just before the consequent, and then employ a theorem handling an implication chain of length one less to reorder the others. (Contributed by Wolf Lammen, 17-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
wl-impchain-com-3.2.1.h1 (𝜃 → (𝜒 → (𝜓𝜑)))
Assertion
Ref Expression
wl-impchain-com-3.2.1 (𝜓 → (𝜃 → (𝜒𝜑)))

Proof of Theorem wl-impchain-com-3.2.1
StepHypRef Expression
1 wl-impchain-com-3.2.1.h1 . . 3 (𝜃 → (𝜒 → (𝜓𝜑)))
21wl-impchain-com-2.3 33597 . 2 (𝜃 → (𝜓 → (𝜒𝜑)))
32wl-impchain-com-1.2 33593 1 (𝜓 → (𝜃 → (𝜒𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-luk1 33559  ax-luk2 33560  ax-luk3 33561
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator