![]() |
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 1153 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
3 | 2 | 3coml 1153 | 1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 927 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: nnacan 6311 le2tri3i 7690 ltaddsublt 8145 div12ap 8258 lemul12b 8419 zdivadd 8934 zdivmul 8935 elfz 9579 fzmmmeqm 9621 fzrev 9647 absdiflt 10656 absdifle 10657 dvds0lem 11249 dvdsmulc 11267 dvds2add 11273 dvds2sub 11274 dvdstr 11276 lcmdvds 11504 psmettri2 12130 xmettri2 12163 |
Copyright terms: Public domain | W3C validator |