| 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 1127 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
| 3 | 2 | 3com13 1125 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: spc3egv 3603 omwordri 8610 oeword 8628 f1oen2g 9009 f1dom2g 9010 f1imaenfi 9235 ordiso 9556 en3lplem2 9653 axdc3lem4 10493 ltasr 11140 adddir 11252 axltadd 11334 pnpcan2 11549 subdir 11697 ltaddsub 11737 leaddsub 11739 mulcan2g 11917 div13 11943 ltdiv2 12154 lediv2 12158 zdiv 12688 xadddir 13338 xadddi2r 13340 fzen 13581 fzrevral2 13653 fzshftral 13655 ssfzoulel 13799 fzind2 13824 flflp1 13847 mulbinom2 14262 digit1 14276 faclbnd5 14337 ccatlcan 14756 elicc4abs 15358 dvdsnegb 16311 muldvds1 16318 muldvds2 16319 dvdscmul 16320 dvdsmulc 16321 dvdscmulr 16322 dvdsmulcr 16323 dvdsgcd 16581 mulgcdr 16587 lcmgcdeq 16649 congr 16701 mulgnnass 19127 gaass 19315 elfm3 23958 mettri 24362 cnmet 24792 addcnlem 24886 bcthlem5 25362 isppw2 27158 vmappw 27159 bcmono 27321 sletr 27803 sltadd1im 28018 colinearalg 28925 ax5seglem1 28943 ax5seglem2 28944 vcdir 30585 vcass 30586 imsmetlem 30709 hvaddcan2 31090 hvsubcan2 31094 dfgcd3 37325 isbasisrelowllem1 37356 ltflcei 37615 fzmul 37748 brcnvrabga 38343 pclfinclN 39952 rabrenfdioph 42825 uun123p2 44830 isosctrlem1ALT 44954 |
| Copyright terms: Public domain | W3C validator |