![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3exp2 | GIF version |
Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Ref | Expression |
---|---|
3exp2.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
3exp2 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp2.1 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) | |
2 | 1 | ex 115 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | 3expd 1226 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: 3anassrs 1231 po2nr 4327 fliftfund 5819 tfrlemibxssdm 6353 tfr1onlembxssdm 6369 tfrcllembxssdm 6382 grpinveu 12997 grpid 12998 grpasscan1 13022 imasgrp2 13067 imasrng 13327 imasring 13431 islmodd 13626 islssmd 13692 mulgghm2 13923 isxmetd 14324 dvidlemap 14637 |
Copyright terms: Public domain | W3C validator |