![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3com23 | Structured version Visualization version GIF version |
Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 9-Apr-2022.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3com23 | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3comr 1290 | . 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com12 1288 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1054 |
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 197 df-an 385 df-3an 1056 |
This theorem is referenced by: 3coml 1292 syld3an2 1413 3anidm13 1424 eqreu 3431 f1ofveu 6685 curry2f 7318 dfsmo2 7489 nneob 7777 f1oeng 8016 suppr 8418 infdif 9069 axdclem2 9380 gchen1 9485 grumap 9668 grudomon 9677 mul32 10241 add32 10292 subsub23 10324 subadd23 10331 addsub12 10332 subsub 10349 subsub3 10351 sub32 10353 suble 10544 lesub 10545 ltsub23 10546 ltsub13 10547 ltleadd 10549 div32 10743 div13 10744 div12 10745 divdiv32 10771 cju 11054 infssuzle 11809 ioo0 12238 ico0 12259 ioc0 12260 icc0 12261 fzen 12396 modcyc 12745 expgt0 12933 expge0 12936 expge1 12937 2cshwcom 13608 shftval2 13859 abs3dif 14115 divalgb 15174 submrc 16335 mrieqv2d 16346 pltnlt 17015 pltn2lp 17016 tosso 17083 latnle 17132 latabs1 17134 lubel 17169 ipopos 17207 grpinvcnv 17530 mulgneg2 17622 oppgmnd 17830 oddvdsnn0 18009 oddvds 18012 odmulg 18019 odcl2 18028 lsmcomx 18305 srgrmhm 18582 ringcom 18625 mulgass2 18647 opprring 18677 irredrmul 18753 irredlmul 18754 isdrngrd 18821 islmodd 18917 lmodcom 18957 rmodislmod 18979 opprdomn 19349 zntoslem 19953 ipcl 20026 maducoevalmin1 20506 rintopn 20762 opnnei 20972 restin 21018 cnpnei 21116 cnprest 21141 ordthaus 21236 kgen2ss 21406 hausflim 21832 fclsfnflim 21878 cnpfcf 21892 opnsubg 21958 cuspcvg 22152 psmetsym 22162 xmetsym 22199 ngpdsr 22456 ngpds2r 22458 ngpds3r 22460 clmmulg 22947 cphipval2 23086 iscau2 23121 dgr1term 24061 cxpeq0 24469 cxpge0 24474 relogbzcl 24557 grpoidinvlem2 27487 grpoinvdiv 27519 nvpncan 27637 nvabs 27655 ipval2lem2 27687 dipcj 27697 diporthcom 27699 dipdi 27826 dipassr 27829 dipsubdi 27832 hlipcj 27895 hvadd32 28019 hvsub32 28030 his5 28071 hoadd32 28770 hosubsub 28804 unopf1o 28903 adj2 28921 adjvalval 28924 adjlnop 29073 leopmul2i 29122 cvntr 29279 mdsymlem5 29394 sumdmdii 29402 supxrnemnf 29662 odutos 29791 tlt2 29792 tosglblem 29797 archiabl 29880 unitdivcld 30075 bnj605 31103 bnj607 31112 gcd32 31763 cgrrflx 32219 cgrcom 32222 cgrcomr 32229 btwntriv1 32248 cgr3com 32285 colineartriv2 32300 segleantisym 32347 seglelin 32348 btwnoutside 32357 clsint2 32449 dissneqlem 33317 ftc1anclem5 33619 heibor1 33739 rngoidl 33953 ispridlc 33999 opltcon3b 34809 cmtcomlemN 34853 cmtcomN 34854 cmt3N 34856 cmtbr3N 34859 cvrval2 34879 cvrnbtwn4 34884 leatb 34897 atlrelat1 34926 hlatlej2 34980 hlateq 35003 hlrelat5N 35005 snatpsubN 35354 pmap11 35366 paddcom 35417 sspadd2 35420 paddss12 35423 cdleme51finvN 36161 cdleme51finvtrN 36163 cdlemeiota 36190 cdlemg2jlemOLDN 36198 cdlemg2klem 36200 cdlemg4b1 36214 cdlemg4b2 36215 trljco2 36346 tgrpabl 36356 tendoplcom 36387 cdleml6 36586 erngdvlem3-rN 36603 dia11N 36654 dib11N 36766 dih11 36871 nerabdioph 37690 monotoddzzfi 37824 fzneg 37866 jm2.19lem2 37874 nzss 38833 sineq0ALT 39487 lincvalsng 42530 reccot 42827 |
Copyright terms: Public domain | W3C validator |