![]() |
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 5682 tz7.7 6411 oalimcl 8596 unbenlem 16941 rnelfm 23976 conway 27858 uspgr2wlkeqi 29680 1pthon2v 30181 spansncvi 31680 atom1d 32381 chirredlem3 32420 finminlem 36300 cvlcvr1 39320 lhpexle2lem 39991 trlord 40551 cdlemkid4 40916 dihord6apre 41238 dihglbcpreN 41282 |
Copyright terms: Public domain | W3C validator |