![]() |
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 412 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | impd 412 | 1 ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: imp44 430 reuop 6293 omordi 8566 omwordri 8572 omass 8580 oewordri 8592 umgrclwwlkge2 29244 upgr4cycl4dv4e 29438 elspansn5 30827 atcvat3i 31649 mdsymlem5 31660 sumdmdlem 31671 cvrat4 38314 2reuimp 45823 sprsymrelfolem2 46161 reupr 46190 |
Copyright terms: Public domain | W3C validator |