![]() |
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 1291 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com13 1289 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1054 |
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 197 df-an 385 df-3an 1056 |
This theorem is referenced by: 3comrOLD 1294 omwordri 7697 oeword 7715 f1oen2g 8014 f1dom2g 8015 ordiso 8462 en3lplem2 8550 axdc3lem4 9313 ltasr 9959 adddir 10069 axltadd 10149 pnpcan2 10359 subdir 10502 ltaddsub 10540 leaddsub 10542 mulcan2g 10719 div13 10744 ltdiv2 10947 lediv2 10951 zdiv 11485 xadddir 12164 xadddi2r 12166 fzen 12396 fzrevral2 12464 fzshftral 12466 ssfzoulel 12602 fzind2 12626 flflp1 12648 mulbinom2 13024 digit1 13038 faclbnd5 13125 ccatlcan 13518 relexpreld 13824 elicc4abs 14103 dvdsnegb 15046 muldvds1 15053 muldvds2 15054 dvdscmul 15055 dvdsmulc 15056 dvdscmulr 15057 dvdsmulcr 15058 dvdsgcd 15308 mulgcdr 15314 lcmgcdeq 15372 coprmdvdsOLD 15414 congr 15425 mulgnnass 17623 mulgnnassOLD 17624 gaass 17776 elfm3 21801 mettri 22204 cnmet 22622 addcnlem 22714 bcthlem5 23171 isppw2 24886 vmappw 24887 bcmono 25047 colinearalg 25835 ax5seglem1 25853 ax5seglem2 25854 vcdir 27549 vcass 27550 imsmetlem 27673 hvaddcan2 28056 hvsubcan2 28060 sletr 32008 dfgcd3 33300 isbasisrelowllem1 33333 ltflcei 33527 fzmul 33667 pclfinclN 35554 rabrenfdioph 37695 uun123p2 39354 isosctrlem1ALT 39484 |
Copyright terms: Public domain | W3C validator |