![]() |
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 1211 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
3 | 2 | 3coml 1211 | 1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 981 |
This theorem is referenced by: nnacan 6527 le2tri3i 8080 ltaddsublt 8542 div12ap 8665 lemul12b 8832 zdivadd 9356 zdivmul 9357 elfz 10028 fzmmmeqm 10072 fzrev 10098 absdiflt 11115 absdifle 11116 dvds0lem 11822 dvdsmulc 11840 dvds2add 11846 dvds2sub 11847 dvdstr 11849 lcmdvds 12093 psmettri2 14181 xmettri2 14214 |
Copyright terms: Public domain | W3C validator |