![]() |
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 417 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
3 | 2 | impd 411 | 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: sylan2d 604 anabsi6 666 mpand 691 2eu3 2711 ralcom2 3326 somo 5405 wereu2 5447 smoel 7856 cfub 9524 cofsmo 9544 grudomon 10092 axpre-sup 10444 leltadd 10978 lemul12b 11351 lbzbi 12189 injresinj 13012 swrdnnn0nd 13858 abslt 14512 absle 14513 o1lo1 14732 o1co 14781 rlimno1 14848 dvdssub2 15488 lublecllem 17431 f1omvdco2 18311 ptpjpre1 21867 iocopnst 23231 ovolicc2lem4 23808 itg2le 24027 ulmcau 24670 cxpeq0 24946 pntrsumbnd2 25829 cvcon3 29748 atexch 29845 abfmpeld 30085 wsuclem 32723 btwntriv2 33084 btwnexch3 33092 isbasisrelowllem1 34188 isbasisrelowllem2 34189 relowlssretop 34196 finxpsuclem 34230 isinf2 34238 finixpnum 34429 fin2solem 34430 ltflcei 34432 poimirlem27 34471 itg2addnclem 34495 unirep 34541 prter2 35569 cvrcon3b 35965 incssnn0 38814 eldioph4b 38914 fphpdo 38920 pellexlem5 38936 pm14.24 40323 icceuelpart 43100 prsprel 43153 sprsymrelfolem2 43159 goldbachthlem2 43212 gbegt5 43430 aacllem 44404 |
Copyright terms: Public domain | W3C validator |