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 413 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜃 → 𝜏)) |
3 | 2 | exp31 420 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: ad5ant2345 1362 tz7.49 8072 supxrun 12699 injresinj 13148 fi1uzind 13845 brfi1indALT 13848 swrdswrdlem 14056 swrdswrd 14057 2cshwcshw 14177 cshwcsh2id 14180 prmgaplem6 16382 cusgrsize2inds 27163 usgr2pthlem 27472 usgr2pth 27473 elwwlks2 27673 rusgrnumwwlks 27681 clwlkclwwlklem2a4 27703 clwlkclwwlklem2 27706 umgrhashecclwwlk 27785 1to3vfriswmgr 27987 frgrnbnb 28000 branmfn 29810 relowlpssretop 34528 broucube 34808 eel0000 40934 eel00001 40935 eel00000 40936 eel11111 40937 climrec 41764 bgoldbtbndlem4 43820 bgoldbtbnd 43821 tgoldbach 43829 isomuspgr 43846 2zlidl 44103 2zrngmmgm 44115 lincsumcl 44384 |
Copyright terms: Public domain | W3C validator |