![]() |
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 421 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 417 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: isofrlem 7337 f1ocnv2d 7659 oelim 8534 zorn2lem7 10497 addrid 11394 initoeu1 17961 termoeu1 17968 issubg4 19025 lmodvsdir 20496 lmodvsass 20497 gsummatr01lem4 22160 dvfsumrlim3 25550 wwlksext2clwwlk 29310 shscli 30570 f1o3d 31851 slmdvsdir 32361 slmdvsass 32362 lshpcmp 37858 |
Copyright terms: Public domain | W3C validator |