|   | 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 412 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜃 → 𝜏)) | 
| 3 | 2 | exp31 419 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: ad5ant2345 1372 tz7.49 8485 supxrun 13358 injresinj 13827 fi1uzind 14546 brfi1indALT 14549 swrdswrdlem 14742 swrdswrd 14743 2cshwcshw 14864 cshwcsh2id 14867 prmgaplem6 17094 cusgrsize2inds 29471 usgr2pthlem 29783 usgr2pth 29784 elwwlks2 29986 rusgrnumwwlks 29994 clwlkclwwlklem2a4 30016 clwlkclwwlklem2 30019 umgrhashecclwwlk 30097 1to3vfriswmgr 30299 frgrnbnb 30312 branmfn 32124 elrspunidl 33456 dfufd2lem 33577 zarcmplem 33880 relowlpssretop 37365 broucube 37661 eel0000 44740 eel00001 44741 eel00000 44742 eel11111 44743 climrec 45618 bgoldbtbndlem4 47795 bgoldbtbnd 47796 tgoldbach 47804 2zlidl 48156 2zrngmmgm 48168 lincsumcl 48348 | 
| Copyright terms: Public domain | W3C validator |