![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3imp1 | Structured version Visualization version GIF version |
Description: Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.) |
Ref | Expression |
---|---|
3imp1.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
3imp1 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imp1.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | 3imp 1098 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏)) |
3 | 2 | imp 397 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: 3an1rs 1421 reupick2 4139 indcardi 9199 ledivge1le 12214 expcan 13235 ltexp2 13236 leexp1a 13241 expnbnd 13316 cshf1 13965 rtrclreclem4 14212 relexpindlem 14214 ncoprmlnprm 15844 xrsdsreclblem 20192 matecl 20639 scmateALT 20727 riinopn 21124 neindisj2 21339 filufint 22136 tsmsxp 22370 ewlkle 26957 uspgr2wlkeq 26997 spthonepeq 27108 wwlksm1edg 27234 wwlksm1edgOLD 27235 clwwisshclwws 27408 clwwlknwwlksn 27431 clwwlkinwwlk 27433 clwwlkinwwlkOLD 27434 wwlksext2clwwlk 27458 3vfriswmgr 27690 homco1 29236 homulass 29237 hoadddir 29239 mblfinlem3 34079 zerdivemp1x 34375 athgt 35615 psubspi 35906 paddasslem14 35992 eluzge0nn0 42364 iccpartigtl 42401 lighneal 42559 isomgrsym 42759 |
Copyright terms: Public domain | W3C validator |