| 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 1126 | . 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
| 3 | 2 | 3com12 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: 3coml 1128 3anidm13 1422 eqreu 3735 f1ofveu 7425 curry2f 8133 dfsmo2 8387 nneob 8694 nadd32 8735 f1oeng 9011 domnsymfi 9240 sdomdomtrfi 9241 domsdomtrfi 9242 php 9247 php3 9249 fodomfir 9368 suppr 9511 infdif 10248 axdclem2 10560 gchen1 10665 grumap 10848 grudomon 10857 mul32 11427 add32 11480 subsub23 11513 subadd23 11520 addsub12 11521 subsub 11539 subsub3 11541 sub32 11543 suble 11741 lesub 11742 ltsub23 11743 ltsub13 11744 ltleadd 11746 div32 11942 div13 11943 div12 11944 divdiv32 11975 cju 12262 infssuzle 12973 ioo0 13412 ico0 13433 ioc0 13434 icc0 13435 fzen 13581 modcyc 13946 expgt0 14136 expge0 14139 expge1 14140 2cshwcom 14854 shftval2 15114 abs3dif 15370 divalgb 16441 submrc 17671 mrieqv2d 17682 pltnlt 18385 pltn2lp 18386 tosso 18464 latnle 18518 latabs1 18520 lubel 18559 ipopos 18581 grpinvcnv 19024 mulgaddcom 19116 mulgneg2 19126 oppgmnd 19373 oddvdsnn0 19562 oddvds 19565 odmulg 19574 odcl2 19583 lsmcomx 19874 srgcom4 20211 srgrmhm 20219 ringcom 20277 mulgass2 20306 opprrng 20345 irredrmul 20427 irredlmul 20428 isdrngrd 20766 isdrngrdOLD 20768 islmodd 20864 lmodcom 20906 rmodislmod 20928 zntoslem 21575 ipcl 21651 evls1fpws 22373 maducoevalmin1 22658 rintopn 22915 opnnei 23128 restin 23174 cnpnei 23272 cnprest 23297 ordthaus 23392 kgen2ss 23563 hausflim 23989 fclsfnflim 24035 cnpfcf 24049 opnsubg 24116 cuspcvg 24310 psmetsym 24320 xmetsym 24357 ngpdsr 24618 ngpds2r 24620 ngpds3r 24622 clmmulg 25134 cphipval2 25275 iscau2 25311 dgr1term 26299 cxpeq0 26720 cxpge0 26725 relogbzcl 26817 negsunif 28087 grpoidinvlem2 30524 grpoinvdiv 30556 nvpncan 30673 nvabs 30691 ipval2lem2 30723 dipcj 30733 diporthcom 30735 dipdi 30862 dipassr 30865 dipsubdi 30868 hlipcj 30930 hvadd32 31053 hvsub32 31064 his5 31105 hoadd32 31802 hosubsub 31836 unopf1o 31935 adj2 31953 adjvalval 31956 adjlnop 32105 leopmul2i 32154 cvntr 32311 mdsymlem5 32426 sumdmdii 32434 supxrnemnf 32772 odutos 32958 tlt2 32959 tosglblem 32964 archiabl 33205 unitdivcld 33900 bnj605 34921 bnj607 34930 fisshasheq 35120 swrdrevpfx 35122 cusgredgex 35127 acycgr1v 35154 gcd32 35749 cgrrflx 35988 cgrcom 35991 cgrcomr 35998 btwntriv1 36017 cgr3com 36054 colineartriv2 36069 segleantisym 36116 seglelin 36117 btwnoutside 36126 clsint2 36330 dissneqlem 37341 ftc1anclem5 37704 heibor1 37817 rngoidl 38031 ispridlc 38077 opltcon3b 39205 cmtcomlemN 39249 cmtcomN 39250 cmt3N 39252 cmtbr3N 39255 cvrval2 39275 cvrnbtwn4 39280 leatb 39293 atlrelat1 39322 hlatlej2 39377 hlateq 39401 hlrelat5N 39403 snatpsubN 39752 pmap11 39764 paddcom 39815 sspadd2 39818 paddss12 39821 cdleme51finvN 40558 cdleme51finvtrN 40560 cdlemeiota 40587 cdlemg2jlemOLDN 40595 cdlemg2klem 40597 cdlemg4b1 40611 cdlemg4b2 40612 trljco2 40743 tgrpabl 40753 tendoplcom 40784 cdleml6 40983 erngdvlem3-rN 41000 dia11N 41050 dib11N 41162 dih11 41267 uzindd 41978 lcmineqlem1 42030 nerabdioph 42820 monotoddzzfi 42954 fzneg 42994 jm2.19lem2 43002 ismnushort 44320 nzss 44336 sineq0ALT 44957 lincvalsng 48333 reccot 49277 |
| Copyright terms: Public domain | W3C validator |