![]() |
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 1122 | . 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
3 | 2 | 3com12 1120 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: 3coml 1124 3anidm13 1417 eqreu 3721 f1ofveu 7413 curry2f 8113 dfsmo2 8368 nneob 8677 nadd32 8718 f1oeng 8992 domnsymfi 9228 sdomdomtrfi 9229 domsdomtrfi 9230 php 9235 php3 9237 suppr 9496 infdif 10234 axdclem2 10545 gchen1 10650 grumap 10833 grudomon 10842 mul32 11412 add32 11464 subsub23 11497 subadd23 11504 addsub12 11505 subsub 11522 subsub3 11524 sub32 11526 suble 11724 lesub 11725 ltsub23 11726 ltsub13 11727 ltleadd 11729 div32 11925 div13 11926 div12 11927 divdiv32 11955 cju 12241 infssuzle 12948 ioo0 13384 ico0 13405 ioc0 13406 icc0 13407 fzen 13553 modcyc 13907 expgt0 14096 expge0 14099 expge1 14100 2cshwcom 14802 shftval2 15058 abs3dif 15314 divalgb 16384 submrc 17611 mrieqv2d 17622 pltnlt 18335 pltn2lp 18336 tosso 18414 latnle 18468 latabs1 18470 lubel 18509 ipopos 18531 grpinvcnv 18971 mulgaddcom 19061 mulgneg2 19071 oppgmnd 19320 oddvdsnn0 19511 oddvds 19514 odmulg 19523 odcl2 19532 lsmcomx 19823 srgcom4 20166 srgrmhm 20174 ringcom 20228 mulgass2 20257 opprrng 20296 irredrmul 20378 irredlmul 20379 isdrngrd 20670 isdrngrdOLD 20672 islmodd 20761 lmodcom 20803 rmodislmod 20825 rmodislmodOLD 20826 opprdomn 21268 zntoslem 21507 ipcl 21582 evls1fpws 22313 maducoevalmin1 22598 rintopn 22855 opnnei 23068 restin 23114 cnpnei 23212 cnprest 23237 ordthaus 23332 kgen2ss 23503 hausflim 23929 fclsfnflim 23975 cnpfcf 23989 opnsubg 24056 cuspcvg 24250 psmetsym 24260 xmetsym 24297 ngpdsr 24558 ngpds2r 24560 ngpds3r 24562 clmmulg 25072 cphipval2 25213 iscau2 25249 dgr1term 26239 cxpeq0 26657 cxpge0 26662 relogbzcl 26751 negsunif 28013 grpoidinvlem2 30387 grpoinvdiv 30419 nvpncan 30536 nvabs 30554 ipval2lem2 30586 dipcj 30596 diporthcom 30598 dipdi 30725 dipassr 30728 dipsubdi 30731 hlipcj 30793 hvadd32 30916 hvsub32 30927 his5 30968 hoadd32 31665 hosubsub 31699 unopf1o 31798 adj2 31816 adjvalval 31819 adjlnop 31968 leopmul2i 32017 cvntr 32174 mdsymlem5 32289 sumdmdii 32297 supxrnemnf 32620 odutos 32784 tlt2 32785 tosglblem 32790 archiabl 32998 unitdivcld 33633 bnj605 34669 bnj607 34678 fisshasheq 34855 swrdrevpfx 34857 cusgredgex 34862 acycgr1v 34890 gcd32 35474 cgrrflx 35714 cgrcom 35717 cgrcomr 35724 btwntriv1 35743 cgr3com 35780 colineartriv2 35795 segleantisym 35842 seglelin 35843 btwnoutside 35852 clsint2 35944 dissneqlem 36950 ftc1anclem5 37301 heibor1 37414 rngoidl 37628 ispridlc 37674 opltcon3b 38806 cmtcomlemN 38850 cmtcomN 38851 cmt3N 38853 cmtbr3N 38856 cvrval2 38876 cvrnbtwn4 38881 leatb 38894 atlrelat1 38923 hlatlej2 38978 hlateq 39002 hlrelat5N 39004 snatpsubN 39353 pmap11 39365 paddcom 39416 sspadd2 39419 paddss12 39422 cdleme51finvN 40159 cdleme51finvtrN 40161 cdlemeiota 40188 cdlemg2jlemOLDN 40196 cdlemg2klem 40198 cdlemg4b1 40212 cdlemg4b2 40213 trljco2 40344 tgrpabl 40354 tendoplcom 40385 cdleml6 40584 erngdvlem3-rN 40601 dia11N 40651 dib11N 40763 dih11 40868 uzindd 41579 lcmineqlem1 41632 nerabdioph 42371 monotoddzzfi 42505 fzneg 42545 jm2.19lem2 42553 ismnushort 43880 nzss 43896 sineq0ALT 44518 lincvalsng 47670 reccot 48375 |
Copyright terms: Public domain | W3C validator |