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

Theorem con3rr3 151
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 148 . 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  160  ax13b  1962  mo2icl  3379  sbcrextOLD  3506  otsndisj  4969  snnen2o  8134  uzwo  11736  ssnn0fi  12767  s3sndisj  13687  hmeofval  21542  alexsubALTlem4  21835  nbuhgr  26220  nbgrnself2  26240  nb3grprlem2  26264  vtxdginducedm1lem4  26419  cvnbtwn  29115  not12an2impnot1  38604
  Copyright terms: Public domain W3C validator