| 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 207 df-an 396 |
| This theorem is referenced by: sylan2d 605 anabsi6 670 mpand 695 2eu3 2654 ralcom2 3377 somo 5631 wereu2 5682 smoel 8400 cfub 10289 cofsmo 10309 grudomon 10857 axpre-sup 11209 leltadd 11747 lemul12b 12124 lbzbi 12978 injresinj 13827 swrdnnn0nd 14694 abslt 15353 absle 15354 o1lo1 15573 o1co 15622 rlimno1 15690 dvdssub2 16338 lublecllem 18405 f1omvdco2 19466 ptpjpre1 23579 iocopnst 24970 ovolicc2lem4 25555 itg2le 25774 ulmcau 26438 cxpeq0 26720 pntrsumbnd2 27611 absslt 28273 cvcon3 32303 atexch 32400 abfmpeld 32664 wsuclem 35826 btwntriv2 36013 btwnexch3 36021 isbasisrelowllem1 37356 isbasisrelowllem2 37357 relowlssretop 37364 finxpsuclem 37398 isinf2 37406 finixpnum 37612 fin2solem 37613 ltflcei 37615 poimirlem27 37654 itg2addnclem 37678 unirep 37721 prter2 38882 cvrcon3b 39278 fltaccoprm 42650 incssnn0 42722 eldioph4b 42822 fphpdo 42828 pellexlem5 42844 pm14.24 44451 traxext 44994 icceuelpart 47423 prsprel 47474 sprsymrelfolem2 47480 goldbachthlem2 47533 gbegt5 47748 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |