![]() |
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 421 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 416 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: wefrc 5444 tz7.7 6099 oalimcl 8043 unbenlem 16077 rnelfm 22249 uspgr2wlkeqi 27116 1pthon2v 27618 spansncvi 29116 atom1d 29817 chirredlem3 29856 conway 32875 finminlem 33277 cvlcvr1 36027 lhpexle2lem 36697 trlord 37257 cdlemkid4 37622 dihord6apre 37944 dihglbcpreN 37988 |
Copyright terms: Public domain | W3C validator |