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 1117 | . 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com12 1115 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: 3coml 1119 3anidm13 1412 eqreu 3719 f1ofveu 7140 curry2f 7794 dfsmo2 7975 nneob 8269 f1oeng 8517 suppr 8924 infdif 9620 axdclem2 9931 gchen1 10036 grumap 10219 grudomon 10228 mul32 10795 add32 10847 subsub23 10880 subadd23 10887 addsub12 10888 subsub 10905 subsub3 10907 sub32 10909 suble 11107 lesub 11108 ltsub23 11109 ltsub13 11110 ltleadd 11112 div32 11307 div13 11308 div12 11309 divdiv32 11337 cju 11623 infssuzle 12320 ioo0 12753 ico0 12774 ioc0 12775 icc0 12776 fzen 12914 modcyc 13264 expgt0 13452 expge0 13455 expge1 13456 2cshwcom 14168 shftval2 14424 abs3dif 14681 divalgb 15745 submrc 16889 mrieqv2d 16900 pltnlt 17568 pltn2lp 17569 tosso 17636 latnle 17685 latabs1 17687 lubel 17722 ipopos 17760 grpinvcnv 18107 mulgaddcom 18191 mulgneg2 18201 oppgmnd 18422 oddvdsnn0 18603 oddvds 18606 odmulg 18614 odcl2 18623 lsmcomx 18907 srgrmhm 19217 ringcom 19260 mulgass2 19282 opprring 19312 irredrmul 19388 irredlmul 19389 isdrngrd 19459 islmodd 19571 lmodcom 19611 rmodislmod 19633 opprdomn 20004 zntoslem 20633 ipcl 20707 maducoevalmin1 21191 rintopn 21447 opnnei 21658 restin 21704 cnpnei 21802 cnprest 21827 ordthaus 21922 kgen2ss 22093 hausflim 22519 fclsfnflim 22565 cnpfcf 22579 opnsubg 22645 cuspcvg 22839 psmetsym 22849 xmetsym 22886 ngpdsr 23143 ngpds2r 23145 ngpds3r 23147 clmmulg 23634 cphipval2 23773 iscau2 23809 dgr1term 24779 cxpeq0 25188 cxpge0 25193 relogbzcl 25279 grpoidinvlem2 28210 grpoinvdiv 28242 nvpncan 28359 nvabs 28377 ipval2lem2 28409 dipcj 28419 diporthcom 28421 dipdi 28548 dipassr 28551 dipsubdi 28554 hlipcj 28616 hvadd32 28739 hvsub32 28750 his5 28791 hoadd32 29488 hosubsub 29522 unopf1o 29621 adj2 29639 adjvalval 29642 adjlnop 29791 leopmul2i 29840 cvntr 29997 mdsymlem5 30112 sumdmdii 30120 supxrnemnf 30420 odutos 30578 tlt2 30579 tosglblem 30584 archiabl 30755 unitdivcld 31044 bnj605 32079 bnj607 32088 fisshasheq 32250 swrdrevpfx 32261 cusgredgex 32266 acycgr1v 32294 gcd32 32881 cgrrflx 33346 cgrcom 33349 cgrcomr 33356 btwntriv1 33375 cgr3com 33412 colineartriv2 33427 segleantisym 33474 seglelin 33475 btwnoutside 33484 clsint2 33575 dissneqlem 34504 ftc1anclem5 34853 heibor1 34971 rngoidl 35185 ispridlc 35231 opltcon3b 36222 cmtcomlemN 36266 cmtcomN 36267 cmt3N 36269 cmtbr3N 36272 cvrval2 36292 cvrnbtwn4 36297 leatb 36310 atlrelat1 36339 hlatlej2 36394 hlateq 36417 hlrelat5N 36419 snatpsubN 36768 pmap11 36780 paddcom 36831 sspadd2 36834 paddss12 36837 cdleme51finvN 37574 cdleme51finvtrN 37576 cdlemeiota 37603 cdlemg2jlemOLDN 37611 cdlemg2klem 37613 cdlemg4b1 37627 cdlemg4b2 37628 trljco2 37759 tgrpabl 37769 tendoplcom 37800 cdleml6 37999 erngdvlem3-rN 38016 dia11N 38066 dib11N 38178 dih11 38283 nerabdioph 39286 monotoddzzfi 39419 fzneg 39459 jm2.19lem2 39467 nzss 40529 sineq0ALT 41151 lincvalsng 44369 reccot 44755 |
Copyright terms: Public domain | W3C validator |