![]() |
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 416. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 416. (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 413 | 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 206 df-an 397 |
This theorem is referenced by: expd 416 odi 8523 nndi 8567 nnmass 8568 ttukeylem5 10446 genpnmax 10940 mulexp 14004 expadd 14007 expmul 14010 cshwidxmod 14688 prmgaplem6 16925 setsstruct 17045 usgredg2vlem2 28072 usgr2trlncl 28606 clwwlkel 28888 clwwlkf1 28891 wwlksext2clwwlk 28899 n4cyclfrgr 29133 5oalem6 30499 atom1d 31193 grpomndo 36323 pell14qrexpclnn0 41165 truniALT 42803 truniALTVD 43140 iccpartigtl 45585 sbgoldbm 45946 2zlidl 46202 rngccatidALTV 46257 ringccatidALTV 46320 nn0sumshdiglemA 46675 |
Copyright terms: Public domain | W3C validator |