| 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 419 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
| 3 | 2 | expd 415 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: isofrlem 7360 f1ocnv2d 7686 oelim 8572 zorn2lem7 10542 addrid 11441 initoeu1 18056 termoeu1 18063 issubg4 19163 lmodvsdir 20884 lmodvsass 20885 gsummatr01lem4 22664 dvfsumrlim3 26074 wwlksext2clwwlk 30076 shscli 31336 f1o3d 32637 slmdvsdir 33222 slmdvsass 33223 lshpcmp 38989 relpfrlem 44974 |
| Copyright terms: Public domain | W3C validator |