|   | 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 459 | . 2 ⊢ ((𝜒 ∧ 𝜓) → (𝜓 ∧ 𝜒)) | |
| 2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 3 | 1, 2 | sylan2 593 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 | 
| This theorem is referenced by: an42s 661 sotr2 5626 somin2 6155 f1elima 7283 f1imaeq 7285 soisoi 7348 isosolem 7367 xpexr2 7941 smoword 8406 unxpdomlem3 9288 fiming 9538 fiinfg 9539 sornom 10317 fin1a2s 10454 mul4r 11430 mulsub 11706 leltadd 11747 ltord1 11789 leord1 11790 eqord1 11791 divmul24 11971 expcan 14209 ltexp2 14210 bhmafibid2 15505 fsum 15756 fprod 15977 isprm5 16744 ramub 17051 setcinv 18135 grpidpropd 18675 gsumpropd2lem 18692 cmnpropd 19809 gsumcom3 19996 unitpropd 20417 lidl1el 21236 1marepvmarrepid 22581 1marepvsma1 22589 ordtrest2 23212 filuni 23893 haustsms2 24145 blcomps 24403 blcom 24404 metnrmlem3 24883 cnmpopc 24955 icoopnst 24969 icccvx 24981 equivcfil 25333 volcn 25641 dvmptfsum 26013 cxple 26737 cxple3 26743 om2noseqlt2 28306 om2noseqf1o 28307 uhgr2edg 29225 lnosub 30778 chirredlem2 32410 metider 33893 ordtrest2NEW 33922 fsum2dsub 34622 finxpreclem2 37391 fin2so 37614 cover2 37722 filbcmb 37747 isdrngo2 37965 crngohomfo 38013 unichnidl 38038 cdleme50eq 40543 dvhvaddcomN 41098 ismrc 42712 prproropf1olem4 47493 | 
| Copyright terms: Public domain | W3C validator |