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

Theorem con3rr3 150
 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 147 . 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  159  ax13b  1951  mo2icl  3352  sbcrextOLD  3479  otsndisj  4904  snnen2o  8034  uzwo  11627  ssnn0fi  12646  s3sndisj  13554  hmeofval  21371  alexsubALTlem4  21664  nb3graprlem2  25981  frgrancvvdeqlem1  26557  frgrancvvdeqlemA  26564  frgrancvvdeqlemC  26566  frgrawopreglem4  26574  2spotdisj  26588  cvnbtwn  28529  not12an2impnot1  37805  nbuhgr  40565  nbgrnself2  40585  nb3grprlem2  40609  2wspiundisj  41166  frgrncvvdeqlem1  41469  frgrwopreglem4  41484  ssdifsn  42228
 Copyright terms: Public domain W3C validator