![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imp41 | Structured version Visualization version GIF version |
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
imp4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
imp41 | ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | imp 405 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
3 | 2 | imp31 416 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: 3anassrs 1357 ad5ant125 1363 ad5ant2345 1367 peano5 7900 peano5OLD 7901 oelim 8555 lemul12a 12105 uzwo 12928 elfznelfzo 13773 injresinj 13789 swrdswrd 14691 2cshwcshw 14812 dvdsprmpweqle 16858 catidd 17663 grpinveu 18939 2ndcctbss 23403 rusgrnumwwlks 29857 erclwwlktr 29904 wwlksext2clwwlk 29939 erclwwlkntr 29953 grpoinveu 30401 spansncvi 31534 sumdmdii 32297 relowlpssretop 36971 matunitlindflem1 37217 unichnidl 37632 linepsubN 39352 pmapsub 39368 cdlemkid4 40534 hbtlem2 42687 2reu8i 46628 ply1mulgsumlem2 47638 |
Copyright terms: Public domain | W3C validator |