![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exp44 | Structured version Visualization version GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp44.1 | ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
exp44 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp44.1 | . . 3 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏) | |
2 | 1 | exp32 419 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 414 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: wefrc 5672 tz7.7 6397 oalimcl 8581 unbenlem 16880 rnelfm 23901 conway 27778 uspgr2wlkeqi 29534 1pthon2v 30035 spansncvi 31534 atom1d 32235 chirredlem3 32274 finminlem 35933 cvlcvr1 38941 lhpexle2lem 39612 trlord 40172 cdlemkid4 40537 dihord6apre 40859 dihglbcpreN 40903 |
Copyright terms: Public domain | W3C validator |