![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ancom2s | Structured version Visualization version GIF version |
Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
an12s.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
ancom2s | ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.22 458 | . 2 ⊢ ((𝜒 ∧ 𝜓) → (𝜓 ∧ 𝜒)) | |
2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 591 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 |
This theorem is referenced by: an42s 659 sotr2 5616 somin2 6136 f1elima 7268 f1imaeq 7270 soisoi 7331 isosolem 7350 xpexr2 7923 smoword 8383 unxpdomlem3 9273 fiming 9519 fiinfg 9520 sornom 10298 fin1a2s 10435 mul4r 11411 mulsub 11685 leltadd 11726 ltord1 11768 leord1 11769 eqord1 11770 divmul24 11946 expcan 14163 ltexp2 14164 bhmafibid2 15443 fsum 15696 fprod 15915 isprm5 16675 ramub 16979 setcinv 18076 grpidpropd 18619 gsumpropd2lem 18636 cmnpropd 19748 gsumcom3 19935 unitpropd 20358 lidl1el 21124 1marepvmarrepid 22493 1marepvsma1 22501 ordtrest2 23124 filuni 23805 haustsms2 24057 blcomps 24315 blcom 24316 metnrmlem3 24793 cnmpopc 24865 icoopnst 24879 icccvx 24891 equivcfil 25243 volcn 25551 dvmptfsum 25923 cxple 26645 cxple3 26651 om2noseqlt2 28193 om2noseqf1o 28194 uhgr2edg 29063 lnosub 30611 chirredlem2 32243 metider 33551 ordtrest2NEW 33580 fsum2dsub 34295 finxpreclem2 36925 fin2so 37136 cover2 37244 filbcmb 37269 isdrngo2 37487 crngohomfo 37535 unichnidl 37560 cdleme50eq 40069 dvhvaddcomN 40624 ismrc 42185 prproropf1olem4 46908 |
Copyright terms: Public domain | W3C validator |