| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > expdcom | Structured version Visualization version GIF version | ||
| Description: Commuted form of expd 415. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 415. (Revised by Wolf Lammen, 28-Jul-2022.) |
| Ref | Expression |
|---|---|
| expd.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
| Ref | Expression |
|---|---|
| expdcom | ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | expd.1 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
| 2 | 1 | com12 32 | . 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃)) |
| 3 | 2 | ex 412 | 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: expd 415 odi 8617 nndi 8661 nnmass 8662 ttukeylem5 10553 genpnmax 11047 mulexp 14142 expadd 14145 expmul 14148 cshwidxmod 14841 prmgaplem6 17094 setsstruct 17213 usgredg2vlem2 29243 usgr2trlncl 29780 clwwlkel 30065 clwwlkf1 30068 wwlksext2clwwlk 30076 n4cyclfrgr 30310 5oalem6 31678 atom1d 32372 grpomndo 37882 pell14qrexpclnn0 42877 truniALT 44561 truniALTVD 44898 iccpartigtl 47410 sbgoldbm 47771 2zlidl 48156 rngccatidALTV 48188 ringccatidALTV 48222 nn0sumshdiglemA 48540 |
| Copyright terms: Public domain | W3C validator |