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 460 | . 2 ⊢ ((𝜒 ∧ 𝜓) → (𝜓 ∧ 𝜒)) | |
2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 592 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: an42s 657 sotr2 5499 somin2 5989 f1elima 7012 f1imaeq 7014 soisoi 7070 isosolem 7089 xpexr2 7612 smoword 7994 unxpdomlem3 8713 fiming 8951 fiinfg 8952 sornom 9688 fin1a2s 9825 mul4r 10798 mulsub 11072 leltadd 11113 ltord1 11155 leord1 11156 eqord1 11157 divmul24 11333 expcan 13523 ltexp2 13524 bhmafibid2 14816 fsum 15067 fprod 15285 isprm5 16041 ramub 16339 setcinv 17340 grpidpropd 17862 gsumpropd2lem 17879 cmnpropd 18847 gsumcom3 19029 unitpropd 19378 lidl1el 19921 1marepvmarrepid 21114 1marepvsma1 21122 ordtrest2 21742 filuni 22423 haustsms2 22674 blcomps 22932 blcom 22933 metnrmlem3 23398 cnmpopc 23461 icoopnst 23472 icccvx 23483 equivcfil 23831 volcn 24136 dvmptfsum 24501 cxple 25205 cxple3 25211 uhgr2edg 26918 lnosub 28464 chirredlem2 30096 metider 31034 ordtrest2NEW 31066 fsum2dsub 31778 finxpreclem2 34554 fin2so 34761 cover2 34872 filbcmb 34898 isdrngo2 35119 crngohomfo 35167 unichnidl 35192 cdleme50eq 37559 dvhvaddcomN 38114 ismrc 39178 prproropf1olem4 43515 |
Copyright terms: Public domain | W3C validator |