![]() |
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 1145 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com13 1144 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: 3comr 1147 nndir 6182 f1oen2g 6401 f1dom2g 6402 ordiso 6635 addassnqg 6843 ltbtwnnqq 6876 nnanq0 6919 ltasrg 7218 recexgt0sr 7221 axmulass 7310 adddir 7381 axltadd 7458 ltleletr 7469 letr 7470 pnpcan2 7624 subdir 7766 div13ap 8057 zdiv 8729 xrletr 9167 fzen 9351 fzrevral2 9412 fzshftral 9414 fzind2 9538 mulbinom2 9904 elicc4abs 10353 dvdsnegb 10592 muldvds1 10600 muldvds2 10601 dvdscmul 10602 dvdsmulc 10603 dvdsgcd 10780 mulgcdr 10786 lcmgcdeq 10844 congr 10861 |
Copyright terms: Public domain | W3C validator |