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 409 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
3 | 2 | imp31 420 | 1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: 3anassrs 1355 ad5ant125 1361 ad5ant2345 1365 peano5 7597 oelim 8151 lemul12a 11490 uzwo 12303 elfznelfzo 13134 injresinj 13150 swrdswrd 14059 2cshwcshw 14179 dvdsprmpweqle 16214 catidd 16943 grpinveu 18130 2ndcctbss 22055 rusgrnumwwlks 27745 erclwwlktr 27792 wwlksext2clwwlk 27828 erclwwlkntr 27842 grpoinveu 28288 spansncvi 29421 sumdmdii 30184 relowlpssretop 34637 matunitlindflem1 34880 unichnidl 35301 linepsubN 36880 pmapsub 36896 cdlemkid4 38062 hbtlem2 39715 2reu8i 43303 ply1mulgsumlem2 44432 |
Copyright terms: Public domain | W3C validator |