![]() |
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 1124 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
3 | 2 | 3com13 1125 | 1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: 3com23 1127 oacan 8496 omlimcl 8526 nnacan 8576 dif1en 9107 dif1enOLD 9109 unfi 9119 en3lplem2 9554 le2tri3i 11290 ltaddsublt 11787 div12 11840 lemul12b 12017 zdivadd 12579 zdivmul 12580 elfz 13436 fzmmmeqm 13480 fzrev 13510 modmulnn 13800 digit2 14145 digit1 14146 faclbnd5 14204 absdiflt 15208 absdifle 15209 dvds0lem 16154 dvdsmulc 16171 dvds2add 16177 dvds2sub 16178 dvdstr 16181 lcmdvds 16489 pospropd 18221 fmfil 23311 elfm 23314 psmettri2 23678 xmettri2 23709 stdbdmetval 23886 nmf2 23965 isclmi0 24477 iscvsi 24508 brbtwn 27890 colinearalglem3 27899 colinearalg 27901 isvciOLD 29564 nvtri 29654 nmooge0 29751 his7 30074 his2sub2 30077 braadd 30929 bramul 30930 cnlnadjlem2 31052 pjimai 31160 atcvati 31370 mdsymlem5 31391 bnj240 33368 bnj1189 33678 hashfundm 33763 cusgredgex 33772 colineardim1 34692 ftc1anclem6 36202 brcnvrabga 36849 oaord3 41670 omord2com 41680 uun123p3 43181 stoweidlem2 44329 sigarperm 45187 leaddsuble 45615 |
Copyright terms: Public domain | W3C validator |