divmulasscomap - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > divmulasscomap		Unicode version

Theorem divmulasscomap 8563

Description: An associative/commutative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)

**Assertion**
Ref	Expression
divmulasscomap	$/\$ $/\$ $/\$ $/\$ #

**Proof of Theorem divmulasscomap**
Step	Hyp	Ref	Expression
1		divmulassap 8562	. 2 $/\$ $/\$ $/\$ $/\$ #
2		mulcom 7855	. . . . 5 $/\$
3	2	3adant3 1002	. . . 4 $/\$ $/\$
4	3	adantr 274	. . 3 $/\$ $/\$ $/\$ $/\$ #
5	4	oveq1d 5836	. 2 $/\$ $/\$ $/\$ $/\$ #
6		simpl2 986	. . . 4 $/\$ $/\$ $/\$ $/\$ #
7		simpl1 985	. . . 4 $/\$ $/\$ $/\$ $/\$ #
8		simp3 984	. . . . . . 7 $/\$ $/\$
9	8	anim1i 338	. . . . . 6 $/\$ $/\$ $/\$ $/\$ # $/\$ $/\$ #
10		3anass 967	. . . . . 6 $/\$ $/\$ # $/\$ $/\$ #
11	9, 10	sylibr 133	. . . . 5 $/\$ $/\$ $/\$ $/\$ # $/\$ $/\$ #
12		divclap 8545	. . . . 5 $/\$ $/\$ #
13	11, 12	syl 14	. . . 4 $/\$ $/\$ $/\$ $/\$ #
14	6, 7, 13	mulassd 7895	. . 3 $/\$ $/\$ $/\$ $/\$ #
15	8	adantr 274	. . . . . 6 $/\$ $/\$ $/\$ $/\$ #
16		simpr 109	. . . . . 6 $/\$ $/\$ $/\$ $/\$ # $/\$ #
17		divassap 8557	. . . . . 6 $/\$ $/\$ $/\$ #
18	7, 15, 16, 17	syl3anc 1220	. . . . 5 $/\$ $/\$ $/\$ $/\$ #
19	18	eqcomd 2163	. . . 4 $/\$ $/\$ $/\$ $/\$ #
20	19	oveq2d 5837	. . 3 $/\$ $/\$ $/\$ $/\$ #
21	14, 20	eqtrd 2190	. 2 $/\$ $/\$ $/\$ $/\$ #
22	1, 5, 21	3eqtrd 2194	1 $/\$ $/\$ $/\$ $/\$ #

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103 $/\$ w3a 963

wceq 1335

wcel 2128 class class class wbr 3965 (class class class)co 5821

cc 7724

cc0 7726

cmul 7731 # cap 8450

cdiv 8539

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-sep 4082 ax-pow 4135 ax-pr 4169 ax-un 4393 ax-setind 4495 ax-cnex 7817 ax-resscn 7818 ax-1cn 7819 ax-1re 7820 ax-icn 7821 ax-addcl 7822 ax-addrcl 7823 ax-mulcl 7824 ax-mulrcl 7825 ax-addcom 7826 ax-mulcom 7827 ax-addass 7828 ax-mulass 7829 ax-distr 7830 ax-i2m1 7831 ax-0lt1 7832 ax-1rid 7833 ax-0id 7834 ax-rnegex 7835 ax-precex 7836 ax-cnre 7837 ax-pre-ltirr 7838 ax-pre-ltwlin 7839 ax-pre-lttrn 7840 ax-pre-apti 7841 ax-pre-ltadd 7842 ax-pre-mulgt0 7843 ax-pre-mulext 7844

This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-nel 2423 df-ral 2440 df-rex 2441 df-reu 2442 df-rmo 2443 df-rab 2444 df-v 2714 df-sbc 2938 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-pw 3545 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3773 df-br 3966 df-opab 4026 df-id 4253 df-po 4256 df-iso 4257 df-xp 4591 df-rel 4592 df-cnv 4593 df-co 4594 df-dm 4595 df-iota 5134 df-fun 5171 df-fv 5177 df-riota 5777 df-ov 5824 df-oprab 5825 df-mpo 5826 df-pnf 7908 df-mnf 7909 df-xr 7910 df-ltxr 7911 df-le 7912 df-sub 8042 df-neg 8043 df-reap 8444 df-ap 8451 df-div 8540

This theorem is referenced by: cncongr2 11972