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 465 | . 2 ⊢ ((𝜒 ∧ 𝜓) → (𝜓 ∧ 𝜒)) | |
2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 491 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
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 386 |
This theorem is referenced by: an42s 870 sotr2 5064 somin2 5531 f1elima 6520 f1imaeq 6522 soisoi 6578 isosolem 6597 xpexr2 7107 2ndconst 7266 smoword 7463 unxpdomlem3 8166 fiming 8404 fiinfg 8405 sornom 9099 fin1a2s 9236 mulsub 10473 leltadd 10512 ltord1 10554 leord1 10555 eqord1 10556 divmul24 10729 expcan 12913 ltexp2 12914 fsum 14451 fprod 14671 isprm5 15419 ramub 15717 setcinv 16740 grpidpropd 17261 gsumpropd2lem 17273 cmnpropd 18202 unitpropd 18697 lidl1el 19218 gsumcom3 20205 1marepvmarrepid 20381 1marepvsma1 20389 ordtrest2 21008 filuni 21689 haustsms2 21940 blcomps 22198 blcom 22199 metnrmlem3 22664 cnmpt2pc 22727 icoopnst 22738 icccvx 22749 equivcfil 23097 volcn 23374 dvmptfsum 23738 cxple 24441 cxple3 24447 uhgr2edg 26100 lnosub 27614 chirredlem2 29250 bhmafibid2 29645 metider 29937 ordtrest2NEW 29969 fsum2dsub 30685 finxpreclem2 33227 fin2so 33396 cover2 33508 filbcmb 33535 isdrngo2 33757 crngohomfo 33805 unichnidl 33830 cdleme50eq 35829 dvhvaddcomN 36385 ismrc 37264 |
Copyright terms: Public domain | W3C validator |