![]() |
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 407 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
3 | 2 | imp31 418 | 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: 3anassrs 1353 ad5ant125 1359 ad5ant2345 1363 peano5 7468 oelim 8017 lemul12a 11352 uzwo 12164 elfznelfzo 12996 injresinj 13012 swrdswrd 13907 2cshwcshw 14027 dvdsprmpweqle 16055 catidd 16784 grpinveu 17899 2ndcctbss 21751 rusgrnumwwlks 27439 erclwwlktr 27486 erclwwlkntr 27536 grpoinveu 27983 spansncvi 29116 sumdmdii 29879 relowlpssretop 34197 matunitlindflem1 34440 unichnidl 34862 linepsubN 36440 pmapsub 36456 cdlemkid4 37622 hbtlem2 39230 2reu8i 42850 ply1mulgsumlem2 43943 |
Copyright terms: Public domain | W3C validator |