|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > imp4c | Structured version Visualization version GIF version | ||
| Description: An importation inference. (Contributed by NM, 26-Apr-1994.) | 
| Ref | Expression | 
|---|---|
| imp4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | 
| Ref | Expression | 
|---|---|
| imp4c | ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | imp4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
| 2 | 1 | impd 410 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) | 
| 3 | 2 | impd 410 | 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: imp44 428 reuop 6312 omordi 8605 omwordri 8611 omass 8619 oewordri 8631 umgrclwwlkge2 30011 upgr4cycl4dv4e 30205 elspansn5 31594 atcvat3i 32416 mdsymlem5 32427 sumdmdlem 32438 cvrat4 39446 2reuimp 47132 sprsymrelfolem2 47485 reupr 47514 grtriprop 47913 isubgr3stgrlem6 47943 | 
| Copyright terms: Public domain | W3C validator |