![]() |
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 418 | . 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: isofrlem 7341 f1ocnv2d 7663 oelim 8538 zorn2lem7 10501 addrid 11400 initoeu1 17967 termoeu1 17974 issubg4 19063 lmodvsdir 20642 lmodvsass 20643 gsummatr01lem4 22382 dvfsumrlim3 25784 wwlksext2clwwlk 29575 shscli 30835 f1o3d 32116 slmdvsdir 32629 slmdvsass 32630 lshpcmp 38163 |
Copyright terms: Public domain | W3C validator |