Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > con3rr3 | Structured version Visualization version GIF version |
Description: Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.) |
Ref | Expression |
---|---|
con3rr3.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
con3rr3 | ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con3rr3.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | con3d 147 | . 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
3 | 2 | com12 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 |