MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con3rr3 Structured version   Visualization version   GIF version

Theorem con3rr3 158
Description: Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
Hypothesis
Ref Expression
con3rr3.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
con3rr3 𝜒 → (𝜑 → ¬ 𝜓))

Proof of Theorem con3rr3
StepHypRef Expression
1 con3rr3.1 . . 3 (𝜑 → (𝜓𝜒))
21con3d 155 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32com12 32 1 𝜒 → (𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  impi  166  dfbi1  215  ax13b  2039  mo2icl  3681  otsndisj  5381  snnen2o  8681  uzwo  12286  ssnn0fi  13333  wrdnfi  13876  s3sndisj  14303  hmeofval  22338  alexsubALTlem4  22630  nbuhgr  27108  nb3grprlem2  27146  vtxdginducedm1lem4  27307  iswwlksnon  27614  clwwlkn  27786  clwwlknon  27850  cvnbtwn  30044  bj-fvimacnv0  34581  not12an2impnot1  41053
  Copyright terms: Public domain W3C validator