![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exp42 | Structured version Visualization version GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp42.1 | ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
exp42 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp42.1 | . . 3 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏) | |
2 | 1 | exp31 411 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 405 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 |
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 199 df-an 386 |
This theorem is referenced by: isofrlem 6818 f1ocnv2d 7120 oelim 7854 zorn2lem7 9612 addid1 10506 initoeu1 16975 termoeu1 16982 issubg4 17926 lmodvsdir 19205 lmodvsass 19206 gsummatr01lem4 20791 dvfsumrlim3 24137 wwlksext2clwwlk 27373 shscli 28701 f1o3d 29950 slmdvsdir 30285 slmdvsass 30286 lshpcmp 35009 |
Copyright terms: Public domain | W3C validator |