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 2732 ralcom2w 3360 ralcom2 3361 somo 5503 wereu2 5545 smoel 7986 cfub 9659 cofsmo 9679 grudomon 10227 axpre-sup 10579 leltadd 11112 lemul12b 11485 lbzbi 12324 injresinj 13146 swrdnnn0nd 14006 abslt 14662 absle 14663 o1lo1 14882 o1co 14931 rlimno1 14998 dvdssub2 15639 lublecllem 17586 f1omvdco2 18505 ptpjpre1 22107 iocopnst 23471 ovolicc2lem4 24048 itg2le 24267 ulmcau 24910 cxpeq0 25188 pntrsumbnd2 26070 cvcon3 29988 atexch 30085 abfmpeld 30327 wsuclem 33009 btwntriv2 33370 btwnexch3 33378 isbasisrelowllem1 34518 isbasisrelowllem2 34519 relowlssretop 34526 finxpsuclem 34560 isinf2 34568 finixpnum 34758 fin2solem 34759 ltflcei 34761 poimirlem27 34800 itg2addnclem 34824 unirep 34869 prter2 35897 cvrcon3b 36293 incssnn0 39186 eldioph4b 39286 fphpdo 39292 pellexlem5 39308 pm14.24 40641 icceuelpart 43473 prsprel 43526 sprsymrelfolem2 43532 goldbachthlem2 43585 gbegt5 43803 aacllem 44830 |
Copyright terms: Public domain | W3C validator |