![]() |
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.) (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 1123 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
3 | 2 | 3com13 1124 | 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: 3com23 1126 oacan 8491 omlimcl 8521 nnacan 8571 dif1en 9100 dif1enOLD 9102 unfi 9112 en3lplem2 9545 le2tri3i 11281 ltaddsublt 11778 div12 11831 lemul12b 12008 zdivadd 12570 zdivmul 12571 elfz 13422 fzmmmeqm 13466 fzrev 13496 modmulnn 13786 digit2 14131 digit1 14132 faclbnd5 14190 absdiflt 15194 absdifle 15195 dvds0lem 16141 dvdsmulc 16158 dvds2add 16164 dvds2sub 16165 dvdstr 16168 lcmdvds 16476 pospropd 18208 fmfil 23279 elfm 23282 psmettri2 23646 xmettri2 23677 stdbdmetval 23854 nmf2 23933 isclmi0 24445 iscvsi 24476 brbtwn 27734 colinearalglem3 27743 colinearalg 27745 isvciOLD 29408 nvtri 29498 nmooge0 29595 his7 29918 his2sub2 29921 braadd 30773 bramul 30774 cnlnadjlem2 30896 pjimai 31004 atcvati 31214 mdsymlem5 31235 bnj240 33180 bnj1189 33490 hashfundm 33575 cusgredgex 33584 colineardim1 34613 ftc1anclem6 36123 brcnvrabga 36770 oaord3 41565 omord2com 41574 uun123p3 43035 stoweidlem2 44175 sigarperm 45033 leaddsuble 45461 |
Copyright terms: Public domain | W3C validator |