![]() |
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 149 | . 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 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 |