![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ancomsd | Structured version Unicode version |
Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.) |
Ref | Expression |
---|---|
ancomsd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ancomsd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 450 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ancomsd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl5bi 217 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 185 df-an 371 |
This theorem is referenced by: sylan2d 482 mpand 675 anabsi6 814 ralcom2 2991 ralxfrd 4617 somo 4786 wereu2 4828 ordtr3 4875 poirr2 5333 smoel 6934 cfub 8533 cofsmo 8553 grudomon 9099 axpre-sup 9451 leltadd 9938 lemul12b 10301 lbzbi 11058 injresinj 11760 abslt 12924 absle 12925 o1lo1 13137 o1co 13186 rlimno1 13253 znnenlem 13616 dvdssub2 13692 lublecllem 15281 f1omvdco2 16077 ptpjpre1 19286 iocopnst 20654 ovolicc2lem4 21145 itg2le 21360 ulmcau 22003 cxpeq0 22266 pntrsumbnd2 22959 cvcon3 25867 atexch 25964 abfmpeld 26147 wsuclem 27929 nofulllem5 28014 btwntriv2 28210 btwnexch3 28218 finixpnum 28585 fin2solem 28586 ltflcei 28590 itg2addnclem 28614 unirep 28777 prter2 29197 incssnn0 29218 eldioph4b 29321 fphpdo 29327 pellexlem5 29345 pm14.24 29857 cvrcon3b 33285 |
Copyright terms: Public domain | W3C validator |