Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3comr | GIF version |
Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3comr | ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3coml 1188 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
3 | 2 | 3coml 1188 | 1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: nnacan 6401 le2tri3i 7865 ltaddsublt 8326 div12ap 8447 lemul12b 8612 zdivadd 9133 zdivmul 9134 elfz 9789 fzmmmeqm 9831 fzrev 9857 absdiflt 10857 absdifle 10858 dvds0lem 11492 dvdsmulc 11510 dvds2add 11516 dvds2sub 11517 dvdstr 11519 lcmdvds 11749 psmettri2 12486 xmettri2 12519 |
Copyright terms: Public domain | W3C validator |