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 419. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 419. (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 416 | 1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: expd 419 odi 8307 nndi 8351 nnmass 8352 ttukeylem5 10127 genpnmax 10621 mulexp 13674 expadd 13677 expmul 13680 cshwidxmod 14368 prmgaplem6 16609 setsstruct 16729 usgredg2vlem2 27314 usgr2trlncl 27847 clwwlkel 28129 clwwlkf1 28132 wwlksext2clwwlk 28140 n4cyclfrgr 28374 5oalem6 29740 atom1d 30434 grpomndo 35770 pell14qrexpclnn0 40391 truniALT 41834 truniALTVD 42171 iccpartigtl 44548 sbgoldbm 44909 2zlidl 45165 rngccatidALTV 45220 ringccatidALTV 45283 nn0sumshdiglemA 45638 |
Copyright terms: Public domain | W3C validator |