| 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 1111 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏)) |
| 3 | 2 | imp 406 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: 3an1rs 1360 reupick2 4331 indcardi 10081 ledivge1le 13106 expcan 14209 ltexp2 14210 leexp1a 14215 expnbnd 14271 cshf1 14848 rtrclreclem4 15100 relexpindlem 15102 ncoprmlnprm 16765 rnglidlmcl 21226 xrsdsreclblem 21430 matecl 22431 scmateALT 22518 riinopn 22914 neindisj2 23131 filufint 23928 tsmsxp 24163 ewlkle 29623 uspgr2wlkeq 29664 spthonepeq 29772 wwlksm1edg 29901 clwwisshclwws 30034 clwwlknwwlksn 30057 clwwlkinwwlk 30059 wwlksext2clwwlk 30076 3vfriswmgr 30297 homco1 31820 homulass 31821 hoadddir 31823 satffunlem 35406 mblfinlem3 37666 zerdivemp1x 37954 athgt 39458 psubspi 39749 paddasslem14 39835 eluzge0nn0 47324 iccpartigtl 47410 lighneal 47598 uhgrimisgrgriclem 47898 uhgrimisgrgric 47899 clnbgrgrimlem 47901 uspgrlimlem3 47957 clnbgr3stgrgrlic 47979 gpgusgralem 48011 |
| Copyright terms: Public domain | W3C validator |