![]() |
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 1123 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com13 1121 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: spc3egv 3587 omwordri 8593 oeword 8611 f1oen2g 8989 f1dom2g 8990 f1dom2gOLD 8991 f1imaenfi 9226 ordiso 9546 en3lplem2 9643 axdc3lem4 10483 ltasr 11130 adddir 11242 axltadd 11324 pnpcan2 11537 subdir 11685 ltaddsub 11725 leaddsub 11727 mulcan2g 11905 div13 11931 ltdiv2 12138 lediv2 12142 zdiv 12670 xadddir 13315 xadddi2r 13317 fzen 13558 fzrevral2 13627 fzshftral 13629 ssfzoulel 13766 fzind2 13791 flflp1 13813 mulbinom2 14226 digit1 14240 faclbnd5 14298 ccatlcan 14709 elicc4abs 15307 dvdsnegb 16259 muldvds1 16266 muldvds2 16267 dvdscmul 16268 dvdsmulc 16269 dvdscmulr 16270 dvdsmulcr 16271 dvdsgcd 16528 mulgcdr 16534 lcmgcdeq 16591 congr 16643 mulgnnass 19077 gaass 19265 elfm3 23903 mettri 24307 cnmet 24737 addcnlem 24829 bcthlem5 25305 isppw2 27097 vmappw 27098 bcmono 27260 sletr 27742 sltadd1im 27953 colinearalg 28798 ax5seglem1 28816 ax5seglem2 28817 vcdir 30453 vcass 30454 imsmetlem 30577 hvaddcan2 30958 hvsubcan2 30962 dfgcd3 36936 isbasisrelowllem1 36967 ltflcei 37214 fzmul 37347 brcnvrabga 37946 pclfinclN 39555 rabrenfdioph 42378 uun123p2 44393 isosctrlem1ALT 44517 |
Copyright terms: Public domain | W3C validator |