Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3comr | Structured version Visualization version GIF version |
Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3comr | ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3coml 1264 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
3 | 2 | 3coml 1264 | 1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: oacan 7515 omlimcl 7545 nnacan 7595 en3lplem2 8395 le2tri3i 10046 ltaddsublt 10533 div12 10586 lemul12b 10759 zdivadd 11324 zdivmul 11325 elfz 12203 fzmmmeqm 12245 fzrev 12273 modmulnn 12550 digit2 12859 digit1 12860 faclbnd5 12947 swrdccatin2 13338 absdiflt 13905 absdifle 13906 dvds0lem 14830 dvdsmulc 14847 dvds2add 14853 dvds2sub 14854 dvdstr 14856 mulmoddvds 14889 lcmdvds 15159 pospropd 16957 fmfil 21558 elfm 21561 psmettri2 21924 xmettri2 21955 stdbdmetval 22129 nmf2 22207 isclmi0 22706 iscvsi 22737 brbtwn 25579 colinearalglem3 25588 colinearalg 25590 isvciOLD 26819 nvtri 26909 nmooge0 27006 his7 27331 his2sub2 27334 braadd 28188 bramul 28189 cnlnadjlem2 28311 pjimai 28419 atcvati 28629 mdsymlem5 28650 bnj240 30018 bnj1189 30331 colineardim1 31338 ftc1anclem6 32660 uun123p3 38059 stoweidlem2 38895 sigarperm 39698 leaddsuble 40343 |
Copyright terms: Public domain | W3C validator |