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

Theorem wl-imim1i 32204
Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Copy of imim1i 60 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.)
Hypothesis
Ref Expression
wl-imim1i.1 (𝜑𝜓)
Assertion
Ref Expression
wl-imim1i ((𝜓𝜒) → (𝜑𝜒))

Proof of Theorem wl-imim1i
StepHypRef Expression
1 wl-imim1i.1 . 2 (𝜑𝜓)
2 ax-luk1 32200 . 2 ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))
31, 2ax-mp 5 1 ((𝜓𝜒) → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-luk1 32200
This theorem is referenced by:  wl-syl  32205  wl-syl5  32206
  Copyright terms: Public domain W3C validator