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 629 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 451 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: wefrc 5032 tz7.7 5666 oalimcl 7527 unbenlem 15450 rnelfm 21567 wwlknimp 26215 spansncvi 27895 atom1d 28596 chirredlem3 28635 finminlem 31482 cvlcvr1 33644 lhpexle2lem 34313 trlord 34875 cdlemkid4 35240 dihord6apre 35563 dihglbcpreN 35607 uspgr2wlkeqi 40856 1pthon2v-av 41320 |
Copyright terms: Public domain | W3C validator |