| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > exp44 | Structured version Visualization version GIF version | ||
| Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
| Ref | Expression |
|---|---|
| exp44.1 | ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏) |
| Ref | Expression |
|---|---|
| exp44 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exp44.1 | . . 3 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏) | |
| 2 | 1 | exp32 420 | . 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: wefrc 5679 tz7.7 6410 oalimcl 8598 unbenlem 16946 rnelfm 23961 conway 27844 uspgr2wlkeqi 29666 1pthon2v 30172 spansncvi 31671 atom1d 32372 chirredlem3 32411 finminlem 36319 cvlcvr1 39340 lhpexle2lem 40011 trlord 40571 cdlemkid4 40936 dihord6apre 41258 dihglbcpreN 41302 |
| Copyright terms: Public domain | W3C validator |