![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3coml | Structured version Visualization version 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 1160 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com13 1158 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 199 df-an 387 df-3an 1113 |
This theorem is referenced by: 3comrOLD 1454 omwordri 7924 oeword 7942 f1oen2g 8245 f1dom2g 8246 ordiso 8697 en3lplem2 8792 axdc3lem4 9597 ltasr 10244 adddir 10354 axltadd 10437 pnpcan2 10649 subdir 10795 ltaddsub 10833 leaddsub 10835 mulcan2g 11013 div13 11038 ltdiv2 11246 lediv2 11250 zdiv 11782 xadddir 12421 xadddi2r 12423 fzen 12658 fzrevral2 12727 fzshftral 12729 ssfzoulel 12864 fzind2 12888 flflp1 12910 mulbinom2 13285 digit1 13299 faclbnd5 13385 ccatlcan 13814 relexpreld 14164 elicc4abs 14443 dvdsnegb 15383 muldvds1 15390 muldvds2 15391 dvdscmul 15392 dvdsmulc 15393 dvdscmulr 15394 dvdsmulcr 15395 dvdsgcd 15641 mulgcdr 15647 lcmgcdeq 15705 congr 15757 mulgnnass 17935 gaass 18087 elfm3 22131 mettri 22534 cnmet 22952 addcnlem 23044 bcthlem5 23503 isppw2 25261 vmappw 25262 bcmono 25422 colinearalg 26216 ax5seglem1 26234 ax5seglem2 26235 vcdir 27972 vcass 27973 imsmetlem 28096 hvaddcan2 28479 hvsubcan2 28483 sletr 32417 dfgcd3 33711 isbasisrelowllem1 33743 ltflcei 33935 fzmul 34074 brcnvrabga 34653 pclfinclN 36020 rabrenfdioph 38217 uun123p2 39859 isosctrlem1ALT 39983 |
Copyright terms: Public domain | W3C validator |