![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ancomsd | Structured version Visualization version GIF 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 | ancomsd.1 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
2 | 1 | expcomd 416 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
3 | 2 | impd 410 | 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 206 df-an 396 |
This theorem is referenced by: sylan2d 604 anabsi6 667 mpand 692 2eu3 2641 ralcom2 3365 somo 5615 wereu2 5663 smoel 8355 cfub 10239 cofsmo 10259 grudomon 10807 axpre-sup 11159 leltadd 11694 lemul12b 12067 lbzbi 12916 injresinj 13749 swrdnnn0nd 14602 abslt 15257 absle 15258 o1lo1 15477 o1co 15526 rlimno1 15596 dvdssub2 16240 lublecllem 18312 f1omvdco2 19353 ptpjpre1 23385 iocopnst 24774 ovolicc2lem4 25359 itg2le 25579 ulmcau 26236 cxpeq0 26516 pntrsumbnd2 27404 absslt 28047 cvcon3 31961 atexch 32058 abfmpeld 32303 wsuclem 35258 btwntriv2 35445 btwnexch3 35453 isbasisrelowllem1 36692 isbasisrelowllem2 36693 relowlssretop 36700 finxpsuclem 36734 isinf2 36742 finixpnum 36929 fin2solem 36930 ltflcei 36932 poimirlem27 36971 itg2addnclem 36995 unirep 37038 prter2 38207 cvrcon3b 38603 sn-negex12 41744 fltaccoprm 41837 incssnn0 41904 eldioph4b 42004 fphpdo 42010 pellexlem5 42026 pm14.24 43646 icceuelpart 46555 prsprel 46606 sprsymrelfolem2 46612 goldbachthlem2 46665 gbegt5 46880 aacllem 48002 |
Copyright terms: Public domain | W3C validator |