![]() |
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 1211 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com13 1210 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 980 |
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 982 |
This theorem is referenced by: 3comr 1213 nndir 6515 f1oen2g 6781 f1dom2g 6782 ordiso 7065 addassnqg 7411 ltbtwnnqq 7444 nnanq0 7487 ltasrg 7799 recexgt0sr 7802 axmulass 7902 adddir 7978 axltadd 8057 ltleletr 8069 letr 8070 pnpcan2 8227 subdir 8373 div13ap 8680 zdiv 9371 xrletr 9838 fzen 10073 fzrevral2 10136 fzshftral 10138 fzind2 10269 mulbinom2 10668 elicc4abs 11135 dvdsnegb 11847 muldvds1 11855 muldvds2 11856 dvdscmul 11857 dvdsmulc 11858 dvdsgcd 12045 mulgcdr 12051 lcmgcdeq 12115 congr 12132 mulgnnass 13097 mettri 14333 cnmet 14490 addcncntoplem 14511 |
Copyright terms: Public domain | W3C validator |