![]() |
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 423 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 419 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: isofrlem 7072 f1ocnv2d 7378 oelim 8142 zorn2lem7 9913 addid1 10809 initoeu1 17263 termoeu1 17270 issubg4 18290 lmodvsdir 19651 lmodvsass 19652 gsummatr01lem4 21263 dvfsumrlim3 24636 wwlksext2clwwlk 27842 shscli 29100 f1o3d 30386 slmdvsdir 30894 slmdvsass 30895 lshpcmp 36284 |
Copyright terms: Public domain | W3C validator |