![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3com12 | Structured version Visualization version GIF version |
Description: Commutation in antecedent. Swap 1st and 2nd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3com12 | ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ancoma 1062 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | |
2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | sylbi 207 | 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: 3comr 1290 3com23 1291 3imp21 1298 3adant2l 1360 3adant2r 1361 brelrng 5387 fresaunres1 6115 fvun2 6309 onfununi 7483 oaword 7674 nnaword 7752 nnmword 7758 ecopovtrn 7893 fpmg 7925 tskord 9640 ltadd2 10179 mul12 10240 add12 10291 addsub 10330 addsubeq4 10334 ppncan 10361 leadd1 10534 ltaddsub2 10541 leaddsub2 10543 ltsub1 10562 ltsub2 10563 div23 10742 ltmul1 10911 ltmulgt11 10921 lediv1 10926 lemuldiv 10941 ltdiv2 10947 zdiv 11485 xltadd1 12124 xltmul1 12160 iooneg 12330 icoshft 12332 fzaddel 12413 fzshftral 12466 modmulmodr 12776 facwordi 13116 abssubge0 14111 climshftlem 14349 dvdsmul1 15050 divalglem8 15170 divalgb 15174 lcmgcdeq 15372 pcfac 15650 mhmmulg 17630 rmodislmodlem 18978 xrsdsreval 19839 cnmptcom 21529 hmeof1o2 21614 ordthmeo 21653 isclmi0 22944 iscvsi 22975 cxplt2 24489 axcontlem8 25896 2clwwlk2clwwlklem2lem2 27329 vcdi 27548 isvciOLD 27563 dipdi 27826 dipsubdi 27832 hvadd12 28020 hvmulcom 28028 his5 28071 bcs3 28168 chj12 28521 spansnmul 28551 homul12 28792 hoaddsub 28803 lnopmul 28954 lnopaddmuli 28960 lnopsubmuli 28962 lnfnaddmuli 29032 leop2 29111 dmdsl3 29302 chirredlem3 29379 atmd2 29387 cdj3lem3 29425 signstfvc 30779 3com12d 32429 cnambfre 33588 sdclem2 33668 addrcom 38996 uun123p1 39353 sineq0ALT 39487 stoweidlem17 40552 sigaras 41365 sigarms 41366 |
Copyright terms: Public domain | W3C validator |