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 1192 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
3 | 2 | 3coml 1192 | 1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 963 |
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 965 |
This theorem is referenced by: nnacan 6459 le2tri3i 7985 ltaddsublt 8446 div12ap 8567 lemul12b 8732 zdivadd 9253 zdivmul 9254 elfz 9918 fzmmmeqm 9960 fzrev 9986 absdiflt 10992 absdifle 10993 dvds0lem 11696 dvdsmulc 11714 dvds2add 11720 dvds2sub 11721 dvdstr 11723 lcmdvds 11955 psmettri2 12728 xmettri2 12761 |
Copyright terms: Public domain | W3C validator |