![]() |
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 1159 | . 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com12 1157 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1111 |
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 199 df-an 387 df-3an 1113 |
This theorem is referenced by: 3coml 1161 syld3an2OLD 1536 3anidm13 1547 eqreu 3623 f1ofveu 6900 curry2f 7537 dfsmo2 7710 nneob 7999 f1oeng 8241 suppr 8646 infdif 9346 axdclem2 9657 gchen1 9762 grumap 9945 grudomon 9954 mul32 10522 add32 10573 subsub23 10606 subadd23 10614 addsub12 10615 subsub 10632 subsub3 10634 sub32 10636 suble 10830 lesub 10831 ltsub23 10832 ltsub13 10833 ltleadd 10835 div32 11030 div13 11031 div12 11032 divdiv32 11059 cju 11346 infssuzle 12054 ioo0 12488 ico0 12509 ioc0 12510 icc0 12511 fzen 12651 modcyc 13000 expgt0 13187 expge0 13190 expge1 13191 2cshwcom 13937 shftval2 14192 abs3dif 14448 divalgb 15501 submrc 16641 mrieqv2d 16652 pltnlt 17321 pltn2lp 17322 tosso 17389 latnle 17438 latabs1 17440 lubel 17475 ipopos 17513 grpinvcnv 17837 mulgneg2 17927 oppgmnd 18134 oddvdsnn0 18314 oddvds 18317 odmulg 18324 odcl2 18333 lsmcomx 18612 srgrmhm 18890 ringcom 18933 mulgass2 18955 opprring 18985 irredrmul 19061 irredlmul 19062 isdrngrd 19129 islmodd 19225 lmodcom 19265 rmodislmod 19287 opprdomn 19662 zntoslem 20264 ipcl 20340 maducoevalmin1 20827 rintopn 21084 opnnei 21295 restin 21341 cnpnei 21439 cnprest 21464 ordthaus 21559 kgen2ss 21729 hausflim 22155 fclsfnflim 22201 cnpfcf 22215 opnsubg 22281 cuspcvg 22475 psmetsym 22485 xmetsym 22522 ngpdsr 22779 ngpds2r 22781 ngpds3r 22783 clmmulg 23270 cphipval2 23409 iscau2 23445 dgr1term 24415 cxpeq0 24823 cxpge0 24828 relogbzcl 24914 grpoidinvlem2 27904 grpoinvdiv 27936 nvpncan 28053 nvabs 28071 ipval2lem2 28103 dipcj 28113 diporthcom 28115 dipdi 28242 dipassr 28245 dipsubdi 28248 hlipcj 28311 hvadd32 28435 hvsub32 28446 his5 28487 hoadd32 29186 hosubsub 29220 unopf1o 29319 adj2 29337 adjvalval 29340 adjlnop 29489 leopmul2i 29538 cvntr 29695 mdsymlem5 29810 sumdmdii 29818 supxrnemnf 30070 odutos 30197 tlt2 30198 tosglblem 30203 archiabl 30286 unitdivcld 30481 bnj605 31512 bnj607 31521 gcd32 32168 cgrrflx 32622 cgrcom 32625 cgrcomr 32632 btwntriv1 32651 cgr3com 32688 colineartriv2 32703 segleantisym 32750 seglelin 32751 btwnoutside 32760 clsint2 32851 dissneqlem 33726 ftc1anclem5 34025 heibor1 34144 rngoidl 34358 ispridlc 34404 opltcon3b 35272 cmtcomlemN 35316 cmtcomN 35317 cmt3N 35319 cmtbr3N 35322 cvrval2 35342 cvrnbtwn4 35347 leatb 35360 atlrelat1 35389 hlatlej2 35444 hlateq 35467 hlrelat5N 35469 snatpsubN 35818 pmap11 35830 paddcom 35881 sspadd2 35884 paddss12 35887 cdleme51finvN 36624 cdleme51finvtrN 36626 cdlemeiota 36653 cdlemg2jlemOLDN 36661 cdlemg2klem 36663 cdlemg4b1 36677 cdlemg4b2 36678 trljco2 36809 tgrpabl 36819 tendoplcom 36850 cdleml6 37049 erngdvlem3-rN 37066 dia11N 37116 dib11N 37228 dih11 37333 nerabdioph 38210 monotoddzzfi 38343 fzneg 38385 jm2.19lem2 38393 nzss 39349 sineq0ALT 39984 lincvalsng 43045 reccot 43390 |
Copyright terms: Public domain | W3C validator |