| 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.) Theorems shortened and reordered. (Revised by Wolf Lammen, 9-Apr-2022.) |
| Ref | Expression |
|---|---|
| 3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| 3comr | ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 2 | 1 | 3com12 1124 | . 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: 3com23 1127 sbciegft 3825 oacan 8586 omlimcl 8616 nnacan 8666 dif1en 9200 dif1enOLD 9202 unfi 9211 en3lplem2 9653 le2tri3i 11391 ltaddsublt 11890 div12 11944 lemul12b 12124 zdivadd 12689 zdivmul 12690 elfz 13553 fzmmmeqm 13597 fzrev 13627 modmulnn 13929 digit2 14275 digit1 14276 faclbnd5 14337 hashfundm 14481 absdiflt 15356 absdifle 15357 dvds0lem 16304 dvdsmulc 16321 dvds2add 16327 dvds2sub 16328 dvdstr 16331 lcmdvds 16645 pospropd 18372 fmfil 23952 elfm 23955 psmettri2 24319 xmettri2 24350 stdbdmetval 24527 nmf2 24606 isclmi0 25131 iscvsi 25162 brbtwn 28914 colinearalglem3 28923 colinearalg 28925 isvciOLD 30599 nvtri 30689 nmooge0 30786 his7 31109 his2sub2 31112 braadd 31964 bramul 31965 cnlnadjlem2 32087 pjimai 32195 atcvati 32405 mdsymlem5 32426 bnj240 34713 bnj1189 35023 cusgredgex 35127 colineardim1 36062 ftc1anclem6 37705 brcnvrabga 38343 oaord3 43305 omord2com 43315 uun123p3 44831 stoweidlem2 46017 sigarperm 46875 leaddsuble 47309 |
| Copyright terms: Public domain | W3C validator |