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 1172 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com13 1171 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 947 |
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 949 |
This theorem is referenced by: 3comr 1174 nndir 6354 f1oen2g 6617 f1dom2g 6618 ordiso 6889 addassnqg 7158 ltbtwnnqq 7191 nnanq0 7234 ltasrg 7546 recexgt0sr 7549 axmulass 7649 adddir 7725 axltadd 7802 ltleletr 7814 letr 7815 pnpcan2 7970 subdir 8116 div13ap 8421 zdiv 9107 xrletr 9559 fzen 9791 fzrevral2 9854 fzshftral 9856 fzind2 9984 mulbinom2 10376 elicc4abs 10834 dvdsnegb 11437 muldvds1 11445 muldvds2 11446 dvdscmul 11447 dvdsmulc 11448 dvdsgcd 11627 mulgcdr 11633 lcmgcdeq 11691 congr 11708 mettri 12469 cnmet 12626 addcncntoplem 12647 |
Copyright terms: Public domain | W3C validator |