Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exp41 | Structured version Visualization version GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp41.1 | ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
exp41 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp41.1 | . . 3 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
2 | 1 | ex 416 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜃 → 𝜏)) |
3 | 2 | exp31 423 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: ad5ant2345 1371 tz7.49 8122 supxrun 12804 injresinj 13261 fi1uzind 13961 brfi1indALT 13964 swrdswrdlem 14167 swrdswrd 14168 2cshwcshw 14288 cshwcsh2id 14291 prmgaplem6 16504 cusgrsize2inds 27407 usgr2pthlem 27716 usgr2pth 27717 elwwlks2 27916 rusgrnumwwlks 27924 clwlkclwwlklem2a4 27946 clwlkclwwlklem2 27949 umgrhashecclwwlk 28027 1to3vfriswmgr 28229 frgrnbnb 28242 branmfn 30052 elrspunidl 31190 zarcmplem 31415 relowlpssretop 35190 broucube 35466 eel0000 41918 eel00001 41919 eel00000 41920 eel11111 41921 climrec 42726 bgoldbtbndlem4 44841 bgoldbtbnd 44842 tgoldbach 44850 isomuspgr 44867 2zlidl 45073 2zrngmmgm 45085 lincsumcl 45353 |
Copyright terms: Public domain | W3C validator |