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

Theorem con3rr3 152
 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 149 . 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  161  ax13b  2120  mo2icl  3537  otsndisj  5112  snnen2o  8305  uzwo  11954  ssnn0fi  12992  s3sndisj  13916  hmeofval  21782  alexsubALTlem4  22074  nbuhgr  26462  nbgrnself2OLD  26482  nb3grprlem2  26506  vtxdginducedm1lem4  26673  iswwlksnon  26982  clwwlkn  27178  clwwlknon  27262  cvnbtwn  29485  not12an2impnot1  39309
 Copyright terms: Public domain W3C validator