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 206 df-an 397 |
This theorem is referenced by: ad5ant2345 1369 tz7.49 8276 supxrun 13050 injresinj 13508 fi1uzind 14211 brfi1indALT 14214 swrdswrdlem 14417 swrdswrd 14418 2cshwcshw 14538 cshwcsh2id 14541 prmgaplem6 16757 cusgrsize2inds 27820 usgr2pthlem 28131 usgr2pth 28132 elwwlks2 28331 rusgrnumwwlks 28339 clwlkclwwlklem2a4 28361 clwlkclwwlklem2 28364 umgrhashecclwwlk 28442 1to3vfriswmgr 28644 frgrnbnb 28657 branmfn 30467 elrspunidl 31606 zarcmplem 31831 relowlpssretop 35535 broucube 35811 eel0000 42340 eel00001 42341 eel00000 42342 eel11111 42343 climrec 43144 bgoldbtbndlem4 45260 bgoldbtbnd 45261 tgoldbach 45269 isomuspgr 45286 2zlidl 45492 2zrngmmgm 45504 lincsumcl 45772 |
Copyright terms: Public domain | W3C validator |