![]() |
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 1102 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏)) |
3 | 2 | imp 444 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 197 df-an 385 df-3an 1074 |
This theorem is referenced by: 3an1rs 1453 reupick2 4056 indcardi 9074 ledivge1le 12114 expcan 13127 ltexp2 13128 leexp1a 13133 expnbnd 13207 cshf1 13776 rtrclreclem4 14020 relexpindlem 14022 ncoprmlnprm 15658 xrsdsreclblem 20014 matecl 20453 scmateALT 20540 riinopn 20935 neindisj2 21149 filufint 21945 tsmsxp 22179 ewlkle 26732 uspgr2wlkeq 26773 spthonepeq 26879 wwlksm1edg 27011 clwwisshclwws 27159 clwwlknwwlksn 27187 clwwlknwwlksnOLD 27188 clwwlkinwwlk 27190 wwlksext2clwwlk 27208 3vfriswmgr 27453 homco1 28990 homulass 28991 hoadddir 28993 mblfinlem3 33779 zerdivemp1x 34077 athgt 35263 psubspi 35554 paddasslem14 35640 eluzge0nn0 41850 iccpartigtl 41887 lighneal 42056 |
Copyright terms: Public domain | W3C validator |