![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3coml | GIF version |
Description: Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3coml | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3com23 1155 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com13 1154 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 930 |
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 932 |
This theorem is referenced by: 3comr 1157 nndir 6316 f1oen2g 6579 f1dom2g 6580 ordiso 6836 addassnqg 7091 ltbtwnnqq 7124 nnanq0 7167 ltasrg 7466 recexgt0sr 7469 axmulass 7558 adddir 7629 axltadd 7706 ltleletr 7717 letr 7718 pnpcan2 7873 subdir 8015 div13ap 8314 zdiv 8991 xrletr 9432 fzen 9664 fzrevral2 9727 fzshftral 9729 fzind2 9857 mulbinom2 10249 elicc4abs 10706 dvdsnegb 11305 muldvds1 11313 muldvds2 11314 dvdscmul 11315 dvdsmulc 11316 dvdsgcd 11493 mulgcdr 11499 lcmgcdeq 11557 congr 11574 mettri 12301 cnmet 12452 |
Copyright terms: Public domain | W3C validator |