![]() |
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 407 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 400 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 |
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 197 df-an 383 |
This theorem is referenced by: wefrc 5243 tz7.7 5890 oalimcl 7794 unbenlem 15815 rnelfm 21973 uspgr2wlkeqi 26775 1pthon2v 27329 spansncvi 28847 atom1d 29548 chirredlem3 29587 conway 32243 finminlem 32645 cvlcvr1 35144 lhpexle2lem 35814 trlord 36375 cdlemkid4 36740 dihord6apre 37063 dihglbcpreN 37107 |
Copyright terms: Public domain | W3C validator |