![]() |
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 1110 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏)) |
3 | 2 | imp 406 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 396 df-3an 1088 |
This theorem is referenced by: 3an1rs 1358 reupick2 4320 indcardi 10042 ledivge1le 13052 expcan 14141 ltexp2 14142 leexp1a 14147 expnbnd 14202 cshf1 14767 rtrclreclem4 15015 relexpindlem 15017 ncoprmlnprm 16671 rnglidlmcl 21070 xrsdsreclblem 21279 matecl 22246 scmateALT 22333 riinopn 22729 neindisj2 22946 filufint 23743 tsmsxp 23978 ewlkle 29294 uspgr2wlkeq 29335 spthonepeq 29441 wwlksm1edg 29567 clwwisshclwws 29700 clwwlknwwlksn 29723 clwwlkinwwlk 29725 wwlksext2clwwlk 29742 3vfriswmgr 29963 homco1 31486 homulass 31487 hoadddir 31489 satffunlem 34855 mblfinlem3 36990 zerdivemp1x 37278 athgt 38790 psubspi 39081 paddasslem14 39167 eluzge0nn0 46478 iccpartigtl 46549 lighneal 46737 isomgrsym 46962 |
Copyright terms: Public domain | W3C validator |