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 1249 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏)) |
3 | 2 | imp 444 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: reupick2 3872 indcardi 8747 ledivge1le 11777 expcan 12775 ltexp2 12776 leexp1a 12781 expnbnd 12855 cshf1 13407 rtrclreclem4 13649 relexpindlem 13651 ncoprmlnprm 15274 xrsdsreclblem 19611 matecl 20050 scmateALT 20137 riinopn 20538 neindisj2 20737 filufint 21534 tsmsxp 21768 spthonepeq 26117 usg2wlkeq 26236 rusgraprop4 26471 vdn0frgrav2 26550 vdn1frgrav2 26552 usgreghash2spot 26596 homco1 28044 homulass 28045 hoadddir 28047 mblfinlem3 32618 zerdivemp1x 32916 athgt 33760 psubspi 34051 paddasslem14 34137 iccpartigtl 39961 lighneal 40066 eluzge0nn0 40350 ewlkle 40807 uspgr2wlkeq 40854 spthonepeq-av 40958 wwlksm1edg 41078 clwwisshclwws 41235 3vfriswmgr 41448 av-extwwlkfablem2 41510 |
Copyright terms: Public domain | W3C validator |